Zenn
Open3

Lean4 でいろいろ試す

lean
lean4
imamurayimamuray

まずはローカルで遊べる環境を作る。

2023年7~9月ごろの記事
https://zenn.dev/labbase/articles/b24dca38e0420d

lean4 に関係するツール[1]

  • elan manages the Lean compiler toolchains, similarly to rustup or ghcup.
  • lake builds Lean packages and their dependencies, similarly to cargo, make, or Gradle.

elan: https://github.com/leanprover/elan
lake: https://github.com/leanprover/lean4/tree/master/src/lake

vscode + devcontainer の環境構築

vscode + devcontainer で作れないか調べた。
GlimpseOfLean に devcontainer の設定があったのでそのまま使うことにした。
https://github.com/PatrickMassot/GlimpseOfLean

GlimpseOfLean の .devcontainer 配下の設定をそのまま使って、ローカルの vscode で devcontainer を立ち上げる。devcontainer 内で elan が使えるようになる。

$ elan --version
elan 3.1.1 (71ddc6633 2024-02-22)

elan を使って Lean Manual の Stting Up Lean のコマンドで lean をダウンロードする。lean と lake が使えるようになる。

$ elan default leanprover/lean4:stable
$ lean --version
Lean (version 4.7.0, x86_64-unknown-linux-gnu, commit 6fce8f7d5cd1, Release)
$ lake --version
Lake version 5.0.0-6fce8f7 (Lean version 4.7.0)

lean プロジェクト作成

https://lean-lang.org/lean4/doc/setup.html#lake を見るとカレントディレクトリでのプロジェクト作成とビルド方法が書かれている。

カレントディレクトリに hellolean プロジェクト作成する場合:

$ lake init hellolean

サブディレクトリにプロジェクト作りたい場合は lake new がある。
lake init や lake new すると同時に git init もされる。[2]

プロジェクトを作ると Hello, World! するサンプルプログラムが作られるのでビルドしてみる。

$ lake build

ビルド結果は ./.lake/build/bin/hellolean にバイナリとして作られるので動かしてみる。

$ ./.lake/build/bin/hellolean
Hello, World!

ビルド結果の動作確認ができた。

詳細は lake のドキュメント にいろいろと書いてある。

脚注

  1. https://lean-lang.org/functional_programming_in_lean/introduction.html#getting-lean ↩︎

  2. Either way, Lake will create the following template directory structure and initialize a Git repository for the package. https://github.com/leanprover/lean4/blob/master/src/lake/README.md#creating-and-building-a-package ↩︎

imamurayimamuray

elan で特定のバージョンに切り替える方法

現在のバージョン表示

elan show

特定のバージョンをインストール（例: 4.9.1）

elan toolchain install 4.9.1

install したバージョンを使用する

elan override set 4.9.1