コマンドライン： lean --print-prefix lean --print-libdir lake print-paths | jq . jq . ./lake-manifest.json cat .git/HEAD cat ~/.elan/update-hashes/* | sort エディタ： #eval Lean.findOLean `Name #check と #eval で InfoViewをよく見る。 set_o…

leanprover/lean4:stable と leanprover/lean4:v4.0.0-m5 という名前のツールチェーンは同じもので、名前だけが違う。どちらも、https://github.com/leanprover/lean4/releases/expanded_assets/v4.0.0-m5 からダウンロードされる。が、elanはそれに気付かず…

lakeはnpmほどには洗練されてないみたいだ。現状では完全な自動ビルドは無理な気がする。原因不明な失敗をすることがある。ビルドの手順は、原理的には次のようなことだと思う。 ./lean-toolcahin を見て、ツールチェーンがインストールされてなければ、elan…