Lean バージョンの指定法¶
Lean のバージョン指定は，project ルートの lean-toolchain に書くのが基本です．
このファイルを commit しておくと，別の計算機で project を開いたときにも同じ Lean バージョンが使われます． 講義資料，論文付録，研究プロジェクトでは，Lean と Mathlib のバージョンを固定することが再現性のために重要です．
一時的に特定バージョンのコマンドを使いたい場合は，Elan の +toolchain 記法を使えます．
ただし，project の通常運用では lean-toolchain を編集して管理する方が分かりやすいです．
lake +v4.30.0 new my_project math のように書いた場合，そのコマンドを実行する lake のバージョンを指定しているのであって，
作られる project の Lean バージョンを恒久的に指定する主な方法は，作成後の lean-toolchain です．
現在使われている toolchain を確認するには次を使います．