elan
インストール
macOS
$ brew install elan-init
$ elan default leanprover/lean4:stable
使い方
バージョン確認
$ elan ---version
$ elan -V
-V: バージョン情報
インストール済みのLeanのバージョン、現在有効なバージョンを表示
$ elan show
$ elan default stable
lean-toolchainなど(?)で設定してあるものを変更せず別のバージョンを動かす
$ elan override set leanprover/lean4-nightly:nightly
mathlib4を使えるようにする
既存のプロジェクトの場合
lakefile.leanに下記を追加
code:memo
require mathlib from git
メモ
leanmake
leanproject
leanpkg
関連