Leanプログラミング
Leanは数学の証明を行うための定理証明支援系システムであるが
同様のシステムであるCoqと異なり 純粋関数型プログラミング言語 でもある。
環境
以下の環境でインストール、及び動作確認を行った。
- OS :
Mac M1 Sonoma 14.7 - lean :
Lean (version 4.13.0, arm64-apple-darwin23.6.0, commit 6d22e0e5cc5a, Release)
インストール
以下のインストールを行う。
- rustup : rust管理マネージャ
- elan : leanバージョンマネージャ
- lake : leanパッケージマネージャ
- lean : lean本体
rustup
まずrustupをインストールする。
brew install rustup-init
rustup-init
~/.zhrcや~/.bashrcなどに以下を追記して、パスを通す。
export PAH=$PARH:"$HOME/.cargo/env"
elan, lean, lake
次にlean関連のコマンド群をインストールする。
以下のコマンドを実行して elan をインストールする
cargo install --git https://github.com/leanprover/elan.git
elan-init
~/.zhrcや~/.bashrcなどに以下を追記して、パスを通す。
export PATH=$PATH:$HOME/.elan/bin
elanリポジトリを最新にした後、lean 4系をインストールする
elan self update
elan default leanprover/lean4:stable
以下のコマンドを実行して、インストールできていることを確認する
lean --version
lake --version
以下のファイルを hello.lean として保存する
def main : IO Unit :=
IO.println "Hello, World"
以下のコマンドを実行すると、"Hello, World"が出力される
lean --run hello.lean
開発環境
vim
以下のパッケージを利用する
ファイルのフォーマットは、NeoVim, coc.nvim でのみ対応しているとのこと
VSCode
以下の拡張機能を導入する
ファイルのフォーマットは設定しても利かないっぽい。
また、デバッグ実行も対応していないので、printデバッグになる模様。
結局、コンソールから lean --runを叩くことになるので、vimで良いような気もする。
Leanプロジェクト
以下のコマンドでlakeを利用してLeanのプロジェクトを作成できる。
lake new my-project
実行すると、以下のファイルやフォルダが作成される
.
├── Main.lean
├── MyProject
│ └── Basic.lean
├── MyProject.lean
├── README.md
├── lake-manifest.json
├── lakefile.toml
└── lean-toolchain
lake buildを実行すると、以下のパスにバイナリが作成される
.lake/build/bin/my_project
実行すると Hello, world! が表示される。
tomlファイル以外の設定方法
以下のlakeのREADMEを参照すると、lakefile.leanを利用すると書いてある
lakefile.leanを利用する場合は、lakefile.tomlは不要なので削除しておく
lakefile.leanの中身を以下ように書き換え、再度 lake build を実行すると、先ほどと同様にバイナリが作成される
import Lake
open Lake DSL
package my_project {
-- add package configuration options here
}
lean_lib MyProject {
-- add library configuration options here
}
@[default_target]
lean_exe my_project {
root := `Main
}
スクリプト
バイナリを作成するだけの用途では lakefile.lean を新規に作成する必要は無いが、
以下のようにスクリプトを追加して、実行することができる。
lakefile.leanに以下のhelloスクリプトを追加する。
...
-- hello スクリプト
script hello do
IO.println "Script!"
return 0
@[default_target]
lean_exe my_project {
...
lake run helloと実行すると Script! と表示される。
lakeによるleanファイルの直接実行
2026/09/20 追記
以下のコマンドで対象ファイルを直接実行することができます。
lake env lean --run {実行ファイル}
VSCodeから実行する場合は、タスク実行を登録しておくと便利です。
Cmd + Shift + Bで「lean: compile and run」を選択すれば実行できます。
tasks.jsonに追記する内容
{
"label": "lean: compile and run",
"type": "shell",
"command": "lake",
"args": ["env", "lean", "--run", "Main.lean"],
"group": {
"kind": "build",
"isDefault": true
},
"presentation": {
"reveal": "always",
"panel": "shared"
},
"problemMatcher": {
"owner": "lean",
"pattern": {
"regexp": "^(.*?):(\\d+):(\\d+): (error|warning): (.*)$",
"file": 1,
"line": 2,
"column": 3,
"severity": 4,
"message": 5
}
}
}
GUIについて
未対応。
やりたい場合は、Webのバックエンドとして利用する感じになると思う。
関数型言語としての利用
以下のサイトに文法がまとまっているので、参考にすること