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! と表示される。
GUIについて
未対応。
やりたい場合は、Webのバックエンドとして利用する感じになると思う。
関数型言語としての利用
以下のサイトに文法がまとまっているので、参考にすること