既存 project を開く

GitHub などから既存 project を取得したら，まず project ルートに移動します．

git clone https://github.com/USER/PROJECT.git
cd PROJECT

Mathlib を使う project なら，通常は次を実行します．

lake update
lake exe cache get
lake build

lake update は lake-manifest.json を更新することがあるため， 単に既存 project を使うだけなら，まず lake exe cache get と lake build で足りることもあります． 共同開発中の project で lake-manifest.json を勝手に更新したくない場合は，実行前に差分が出てもよいか確認してください．

VS Code で開くときは，LeanMathNote/ のようなソースディレクトリではなく，lakefile.toml と lean-toolchain がある project ルートを開きます．