lake - pogi-log

lake

Lean 4のlakeについて

プロジェクトの作成

lake initでカレントディレクトリにプロジェクトを作成

$ lake init my-lean-project

lake newで新しいディレクトリにプロジェクトを作成

$ lake new my-lean-project

パッケージのアップデート

$ lake update

$ lake exe cache clean

キャッシュされたビルド済みファイルをダウンロードする

$ lake exe cache get

$ lake build -v | tee "$(date +%Y-%m-%d_%H-%M-%S)_build.log"

-v: --verboseオプション。デバッグ用にメッセージの量を増やす。

warning解消

何かガチャガチャしてたら以下のwarningが出てしまった。

code:memo

PS D:\02_Area\ghworkspace\language\lean\mathematics_in_lean> lake clean

warning: mathlib: repository '.\.\.lake/packages\mathlib' has local changes

warning: batteries: repository '.\.\.lake/packages\batteries' has local changes

mathmatics_in_lean/の.lakeを削除してlake exe cache getしたら治った。

code:memo

PS D:\02_Area\ghworkspace\language\lean\mathematics_in_lean> lake exe cache get

info: mathlib: cloning https://github.com/leanprover-community/mathlib4 to '.\.\.lake/packages\mathlib'

info: batteries: cloning https://github.com/leanprover-community/batteries to '.\.\.lake/packages\batteries'

info: aesop: cloning https://github.com/leanprover-community/aesop to '.\.\.lake/packages\aesop'

info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4 to '.\.\.lake/packages\proofwidgets'

info: Cli: cloning https://github.com/leanprover/lean4-cli to '.\.\.lake/packages\Cli'

info: importGraph: cloning https://github.com/leanprover-community/import-graph.git to '.\.\.lake/packages\importGraph'

No files to download

Decompressing 4539 file(s)

unpacked in 54602 ms

確認用

Q. lake

参考