Elan, Lean, Lake

Lean project を扱うときに出てくる主な道具は次の 3 つです．

名前	役割
elan	Lean toolchain manager．どの Lean バージョンを使うかを選ぶ．
lean	Lean 本体．.lean ファイルを読み，型検査や elaboration を行う．
lake	Lean の package manager / build tool．project 作成，依存関係，ビルドを管理する．

通常，ユーザーが直接呼び出す lean や lake は Elan の proxy です． カレントディレクトリか親ディレクトリに lean-toolchain があれば，Elan はそこに書かれた toolchain を使います．

たとえばこの project の lean-toolchain は次のような 1 行のファイルです．

leanprover/lean4:v4.30.0

この指定により，この project では Lean 4.30.0 系の lean と lake が使われます．