次のパッケージをトップレベルパッケージ（依存パッケージではなく）git clone でインストールする。
- "leancolls" : https://github.com/jamesgallicchio/leancolls
インストールしてすぐ気がつくのは：
- ./lean_packages/ というディレクトリがある。./lake-packages/ ではない。
- ./lean_packages/manifest.json がある。./lean-manifest.json ではない。
- lean-toolcahin は leanprover/lean4:nightly-2022-10-09
- lakefile.lean 内の属性が @[defaultTarget]、@[default_target] ではない。
- lakeバージョンは、Lake version 4.0.0 (Lean version 4.0.0-nightly-2022-10-09) 。パッケージ指定のツールチェーンのバージョン。
lake -v build すると、
LeanColls > lake -v build info: > git fetch origin # in directory .\lean_packages\std error: .\lean_packages\std\lakefile.lean:9:2: error: unknown attribute [default_target] error: .\lean_packages\std\lakefile.lean:12:2: error: unknown attribute [default_target] error: .\lean_packages\std\lakefile.lean: package configuration has errors
./lean_packages/ の下に、mathlibとstdがコピーされている。
LeanColls > cat .\lean_packages\mathlib\lean-toolchain leanprover/lean4:nightly-2022-10-09 LeanColls > cat .\lean_packages\std\lean-toolchain leanprover/lean4:nightly-2023-01-10
mathlibはバージョンがあっているが、stdが新しいのでダメだ。古いlakeでは、変更された属性 @[default_target] が解釈できない。
stdのビルドを、./lean_packages/std/ で手動で行う。成功。
LeanColls/ に昇って、lake build（実際は lean-build.ps1）すると、同じ失敗。既にビルド済みなのに、自分でビルドしようとする。拉致が開かない。いや、ビルドするじゃなくて、依存グラフを作ろうと試みて失敗か。lakefile.lean の構文が変わると破綻する。
stdのバージョンは昔のものにすればいけるかも。git log で探して、git checkout ハッシュ値でデタッチトヘッドを作る。
std > git checkout 6488a2a Previous HEAD position was 5770b60 feat: support priorities in ext (#84) HEAD is now at 6488a2a chore: update nightly 09-11 (#7) std > git branch * (HEAD detached at 6488a2a) main
lakefile.lean の属性は @[defaultTarget] だ。
LeanColls/ に昇って、lake build（実際は lean-build.ps1）する。gitでリビジョンを戻されてしまった。
LeanColls > lean-build info: > git fetch origin # in directory .\lean_packages\std info: updating .\lean_packages\std to revision 5770b609aeae209cb80ac74655ee8c750c12aabd info: > git checkout --detach 5770b609aeae209cb80ac74655ee8c750c12aabd # in directory .\lean_packages\std info: stderr: Previous HEAD position was 6488a2a chore: update nightly 09-11 (#7) HEAD is now at 5770b60 feat: support priorities in ext (#84) error: .\lean_packages\std\lakefile.lean:9:2: error: unknown attribute [default_target] error: .\lean_packages\std\lakefile.lean:12:2: error: unknown attribute [default_target] error: .\lean_packages\std\lakefile.lean: package configuration has errors
std > git branch * (HEAD detached at 5770b60) main
(HEAD detached at 5770b60) は最新版のデタッチトヘッド。
もし、lean_packages/manifest.json が効いているなら、
{ "url": "https://github.com/leanprover/std4", "rev": "a7237a4a4a7dd520ba1425295306bc1b4f754577", "name": "std", "inputRev": "main" }
以下のコミットがダウンロードされるはず。
commit a7237a4a4a7dd520ba1425295306bc1b4f754577
Author: Mario Carneiro <di.gama@gmail.com>
Date: Sun Oct 9 08:14:29 2022 -0400
feat: RBMap.{filter, sdiff}
なんかおかしいが、よくわからん。
ちなみにツールチェーンは：
LeanColls > elan toolchain list leanprover-community/lean:3.23.0 leanprover-community/lean:nightly leanprover-community/lean:stable leanprover/lean4:nightly leanprover/lean4:nightly-2022-07-06 leanprover/lean4:nightly-2022-10-09 leanprover/lean4:nightly-2022-11-20 leanprover/lean4:nightly-2022-12-02 leanprover/lean4:nightly-2022-12-16 leanprover/lean4:nightly-2022-12-22 leanprover/lean4:nightly-2022-12-24 leanprover/lean4:nightly-2023-01-10 leanprover/lean4:stable (default) leanprover/lean4:v4.0.0-m5
ツールチェーンを削除しようとしたら、
LeanColls > elan toolchain uninstall leanprover/lean4:nightly-2022-10-09 info: uninstalling toolchain 'leanprover/lean4:nightly-2022-10-09' error: could not remove 'install' directory: 'C:\Users\m-hiyama\.elan\toolchains\leanprover--lean4---nightly-2022-10-09' info: caused by: アクセスが拒否されました。 (os error 5)
elan のデフォルトを最新のナイトリィビルドにして、新しく作った use-Cli-2/ で作業した。
use-cli-2 > lean-build error: dependency Cli of ﾂｫuse-cli-2ﾂｻ not in manifest, use `lake update` to update use-cli-2 > lake update cloning https://github.com/mhuisi/lean4-cli to .\lake-packages\Cli error: .\.\lake-packages\Cli\lakefile.lean:6:2: error: unknown attribute [defaultTarget] error: .\.\lake-packages\Cli\lakefile.lean: package configuration has errors
やはり、バージョンのミスマッチでビルドできない。
