演習問題

1. 空き容量を確認してください．Mathlib を含む project を作る前に，7.2 GB 程度の余裕があるか確認します．

   df -h .
   

2. Mathlib を含まない project を一時ディレクトリに作り，lake build してください．

   cd /tmp
   lake new lean_sandbox
   cd lean_sandbox
   lake build
   

3. Mathlib を含む project を作る手順を，実行せずに説明してください．

   lake new lean_math_sandbox math
   cd lean_math_sandbox
   lake update
   lake exe cache get
   

4. lean-toolchain を開き，どの Lean バージョンが指定されているか確認してください．

   cat lean-toolchain
   elan show
   

5. この project の lakefile.toml を読み，[[lean_lib]] と [[require]] が何を指定しているか説明してください．

6. lake clean を実行すると何が消えるか，実行前に説明してください． 講義中に実行する場合は，git status --short と du -sh .lake を先に確認してください．