まとめ

Lean project は，Lean ファイルの置き場というだけでなく，Lean バージョン，依存関係，module，ビルド成果物をまとめて管理する単位です．

• Lean バージョンは lean-toolchain で固定する．
• Mathlib なしなら lake new my_project でよい．
• Mathlib ありなら lake new my_project math の後に lake update と lake exe cache get を実行する．
• 既存 project に Mathlib を追加するときは，lean-toolchain と Mathlib revision を対応させる．
• lake build，lake env lean，lake clean の役割を区別する．

この章の内容を押さえると，次章の Lean の内部構造や build artifact の説明を読みやすくなります．