プロジェクトのファイル構造

Lean プロジェクトは，通常 Lake workspace として管理されます． このプロジェクトでは，主なファイルは次のような役割を持ちます．

lean-toolchain        使用する Lean toolchain の指定
lakefile.toml         package，依存関係，ライブラリ target の設定
lake-manifest.json    依存パッケージの具体的な revision の固定
LeanMathNote.lean     ライブラリのルート module
LeanMathNote/         Lean ソースファイル
.lake/                Lake が管理する依存関係とビルド成果物

lake-manifest.json は依存関係のバージョンを固定するため，通常はソース管理に含めます． 一方，.lake/ はビルド成果物やダウンロード済み依存関係を含む作業ディレクトリなので，普通はソース管理に含めません．

これらのファイルをどのように作るか，Mathlib をどう追加するか，lake clean などの操作をどう使うかは Chapter 05 で扱います． ここでは，module を import するときに .lean ファイルが .olean として再利用される，という処理の流れだけを意識してください．