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
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
No files to download
Decompressing 4539 file(s)
unpacked in 54602 ms
確認用
Q. lake
関連
調査用
/pogi-log/Wikipedia.icon
/pogi-log/Wikipedia.icon