よくある失敗

Lean project の操作でよくある失敗をまとめます．

• lakefile.toml がある directory ではなく，その下のソース directory を VS Code で開いている．
• lean-toolchain と Mathlib の revision が対応していない．
• lake update 後に lake exe cache get を実行しておらず，Mathlib を手元で長時間ビルドしている．
• 空き容量が足りない．Mathlib project では 7.2 GB 程度の余裕を見込む．
• lake update によって lake-manifest.json が変わったことに気づかず commit してしまう．
• lake clean を cache 削除コマンドだと思っている．これは主に build outputs を消すためのコマンドである．

困ったときは，まず次を確認します．

pwd
ls
cat lean-toolchain
lake --version
lake build
git status --short