Chapter 05: Lean Project の作成と操作¶
この章では，Lean project を新しく作る方法，既存 project を開く方法，Lean のバージョンを指定する方法， Mathlib を依存関係として追加する方法，Lake の基本操作を説明します．
Lean のファイルは，単独の .lean ファイルとして扱うより，基本的には project の中で扱います．
project は，lean-toolchain，lakefile.toml または lakefile.lean，lake-manifest.json，
ソースディレクトリ，.lake/ 以下の依存関係とビルド成果物をまとめて管理する単位です．
参考:
- Lean Community, Lean projects: https://leanprover-community.github.io/install/project.html
- Lean のインストール方法・elan と Lake の使い方，Lean プロジェクトの作り方: https://aconite-ac.github.io/how_to_install_lean/lake-package-manager/how-to-create-project.html
Mathlib を含む Lean project は容量をかなり使います．
Mathlib の依存パッケージ，ビルド済みキャッシュ，.lake/ 以下の成果物を含めると，少なくとも 7.2 GB 程度の空き容量を見込んでください（2026年6月時点の実績）．
空き容量が少ない状態で lake update や lake exe cache get を実行すると，途中で失敗したり，壊れたキャッシュが残ったりします．