Lake の基本操作

よく使う Lake コマンドをまとめます．

lake build                 # project 全体をビルドする
lake build MyProject.Basic # 特定 module / target をビルドする
lake env lean Foo.lean     # project の依存関係を含む環境で Lean を起動する
lake update                # 依存関係を解決し lake-manifest.json を更新する
lake exe cache get         # Mathlib のビルド済みキャッシュを取得する
lake clean                 # この package の build outputs を削除する

lake clean は，ビルド成果物を消して作り直したいときに使います． 典型的には .lake/build/ 以下の成果物が対象であり，Lean toolchain そのものや， Mathlib の全キャッシュを完全に削除するためのコマンドではありません． 依存関係や cache まで含めて大きく掃除したい場合は，何を消すかを理解してから手動で行ってください．

容量を確認したいときは，たとえば次のようにします．

du -sh .lake
df -h .

macOS や Linux では，.lake/ が project 内で大きくなりやすいディレクトリです． 不要になった実験 project は，project ディレクトリごと削除して構いません． 一方で，作業中の project の .lake/ を消すと，依存関係やビルド成果物を再取得・再ビルドする必要があります．