Mathlib を含む project を作る

数学の形式化では，ほとんどの場合 Mathlib を使います． Mathlib 付きの project は次で作ります．

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

math は，Mathlib を依存関係に含める template です． これにより，project 内の Lean ファイルで

import Mathlib

または

import Mathlib.Topology.Basic

のように書けるようになります．

lake update は依存関係を解決し，lake-manifest.json を更新します． lake exe cache get は Mathlib のビルド済みキャッシュを取得します． Mathlib 全体を手元で最初からビルドすると時間がかかるため，通常はキャッシュを取得してから作業します．

注意: Mathlib を含む project では，.lake/ と Mathlib cache に大きな容量が必要です． 少なくとも 7.2 GB 程度の空き容量を確保してから作成してください．