Leanには強力な数学用ライブラリ Mathlib がありますが，これを利用するためには，プロジェクトディレクトリを作成する必要があります．この記事では，Lean
4における数学用ライブラリ Mathlib を使った証明プログラムを書くためのプロジェクトディレクトリの作成方法を述べます．Leanプロジェクトの作り方のページに書かれている手順に従い，プロジェクトを作成した記録を以下に述べます．また，すでにLean4をインストールされていることを想定していますので，Lean4自体のインストール手順については触れません．
作業は M1 Mac 上で実施しました．Lean のインストールはvscodeの拡張機能である lean4 を用いて行っています．
参考リンクに従い作業を進めてみる．．．
vscode をインストールすると，Leanプロジェクト管理ツールである，elan が ~/.elan/bin/にインストールされていますので，以下のコマンドでツールをアップデートします．
$ elan update
info: syncing channel updates for 'stable'
info: latest update on stable, lean version v4.0.0-m5
info: downloading component 'lean'
Total: 124.9 MiB Speed: 1.5 MiB/s
info: installing component 'lean'
info: syncing channel updates for 'nightly'
info: latest update on nightly, lean version nightly-2023-09-05
info: downloading component 'lean'
Total: 170.2 MiB Speed: 2.4 MiB/s
info: installing component 'lean'
info: checking for self-updates
stable updated - Lean (version 4.0.0, commit 7dbfaf9b7519, Release)
leanprover/lean4:nightly updated - Lean (version 4.0.0-nightly-2023-09-05, commit 84bf315ac89b, Release)
アップデートが完了したらプロジェクトフォルダ my_project を作成したいディレクトリに移動して，以下のコマンドを実行します．
次のコマンドを実行し、作成したLeanプロジェクト内に移動します。
$ lake new my_project math
my_project 内に移動すると、以下のようなファイルが作成されています。
MyProject.lean lakefile.lean
MyProject.lean の中身は
def hello := "world"⏎
lakefile.lean の中身は
import Lake
open Lake DSL
package my_project {
-- add any package configuration options here
}
require mathlib from git
"https://github.com/leanprover-community/mathlib4.git"
@[defaultTarget]
lean_lib MyProject {
-- add any library configuration options here
}
となっていました．
my_project フォルダ内で lake update します．すると．．．
$ lake update
mathlib: no manifest entry; deleting ./lean_packages/mathlib and cloning again
cloning https://github.com/leanprover-community/mathlib4.git to ./lean_packages/mathlib
error: ./lean_packages/mathlib/lakefile.lean:27:2: error: unknown attribute [default_target]
error: ./lean_packages/mathlib/lakefile.lean:30:2: error: 'weakLeanArgs' is not a field of structure 'Lake.LeanLibConfig'
error: ./lean_packages/mathlib/lakefile.lean:51:2: error: 'weakLeanArgs' is not a field of structure 'Lake.LeanLibConfig'
error: ./lean_packages/mathlib/lakefile.lean: package configuration has errors
となりました．(2023-09-06 現在)
ツールのバージョンは以下のとおりです．
$ elan --version
elan 2.0.1 (04475bbb5 2023-07-24)
$ lake --version
Lake version 4.0.0 (Lean version 4.0.0, commit 7dbfaf9b751917a7fe020485bf57f41fdddcaafa)
$ lean --version
Lean (version 4.0.0, commit 7dbfaf9b7519, Release)
さて，どうしたものか．
leanをバックデートする
数学系のためのLean勉強会の教材 で Mathlib を使ったときの lean のバージョンが 4.0.0-rc4 だったのを思い出し，elan でバージョンを leanprover/lean4:v4.0.0-rc4 に戻せるかを試してみます．
まず，elan show で現在のバージョンを確認します．
$ elan show
installed toolchains
--------------------
stable (default)
leanprover/lean4:nightly
leanprover/lean4:nightly-2023-08-19
leanprover/lean4:v4.0.0-rc4
active toolchain
----------------
stable (default)
Lean (version 4.0.0, commit 7dbfaf9b7519, Release)
現在のバージョンは stable で，leanprover/lean4:v4.0.0-rc4 がインストールされていることがわかったので，elan default でバージョンを leanprover/lean4:v4.0.0-rc4 に変更します．
$ elan default leanprover/lean4:v4.0.0-rc4
info: using existing install for 'leanprover/lean4:v4.0.0-rc4'
info: default toolchain set to 'leanprover/lean4:v4.0.0-rc4'
leanprover/lean4:v4.0.0-rc4 unchanged - Lean (version 4.0.0-rc4, commit a7efe5b60e86, Release)
先に作成した my_project フォルダを削除して，もう一度作成してみます．
$ lake new my_project math
my_project 内に移動すると、以下のようなファイルが作成されています．
MyProject.lean lakefile.lean lean-toolchain
先程と異なり lean-toolchain が追加されています．
MyProject.lean の中身は
def hello := "world"⏎
lakefile.lean の中身は
import Lake
open Lake DSL
package my_project {
-- add any package configuration options here
}
require mathlib from git
"https://github.com/leanprover-community/mathlib4.git"
@[default_target]
lean_lib MyProject {
-- add any library configuration options here
}
@[default_target]が違う．．．
lean-toolchain の中身は
leanprover/lean4:v4.0.0-rc4
でした．この状態で lake update します．
$ lake update
cloning https://github.com/leanprover-community/mathlib4.git to ./lake-packages/mathlib
cloning https://github.com/EdAyers/ProofWidgets4 to ./lake-packages/proofwidgets
cloning https://github.com/mhuisi/lean4-cli.git to ./lake-packages/Cli
cloning https://github.com/gebner/quote4 to ./lake-packages/Qq
cloning https://github.com/JLimperg/aesop to ./lake-packages/aesop
cloning https://github.com/leanprover/std4 to ./lake-packages/std
エラーがでなかった！続いて依存バイナリファイルのダウンロードをしてみます．
$ lake exe cache get
info: Downloading proofwidgets/v0.0.13/macOS-64.tar.gz
info: Unpacking proofwidgets/v0.0.13/macOS-64.tar.gz
info: [1/9] Building Cache.IO
info: [2/9] Compiling Cache.IO
info: [2/9] Building Cache.Hashing
info: [3/9] Compiling Cache.Hashing
info: [3/9] Building Cache.Requests
info: [5/9] Compiling Cache.Requests
info: [5/9] Building Cache.Main
info: [7/9] Compiling Cache.Main
info: [9/9] Linking cache
info: stderr:
ld64.lld: warning: /usr/lib/system/libsystem_kernel.dylib has version 13.5.0, which is newer than target minimum of 13.0.0
ld64.lld: warning: /usr/lib/system/libsystem_platform.dylib has version 13.5.0, which is newer than target minimum of 13.0.0
ld64.lld: warning: /usr/lib/system/libsystem_pthread.dylib has version 13.5.0, which is newer than target minimum of 13.0.0
Attempting to download 3714 file(s)
Downloaded: 3714 file(s) [attempted 3714/3714 = 100%] (100% success)
Decompressing 3714 file(s)
unpacked in 5179 ms
というようにうまくいきました．(なんか warning 出てますが目をつぶります)
これで，Mathlib を import できるプロジェクトディレクトリが完成しました．
さいごに
stable のバージョンでは，デフォルトターゲットの属性表記が @[defaultTarget] というキャメル表記になっており，それまで（少なくとも leanprover/lean4:v4.0.0-rc4 まで）のスネーク表記との互換問題が起きているように見えます．少なくとも Mathlib は @[default_target] のまま．ということで，どちらがどちらの表記に合わせるのかわかりませんが，早期修正を願います．．．
参考リンク：
Leave a Reply