概要
この記事では、Lean4のセットアップについて説明します。
関連記事
前の記事「Lean4アドベンドカレンダーことはじめ」
次の記事「Lean4で計算を定義してみる」
前提条件
- Linux上またはpodman/Docker上でのセットアップを想定しています。
Lean4のインストール
基本的には、以下のような流れでLean4をインストールします。
今の時代は便利なもので、Lean4をpodmanコンテナで動かすための環境を構築してください とgithub copilotにお願いすれば、動くものがでてきます。
elanのインストール
Lean4のインストールには、elanというツールを使用します。以下のコマンドでelanをインストールします。
LEAN_VERSION=v4.12.0
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain $LEAN_VERSION
環境変数の設定
elanのインストール後、パスを通します。
source $HOME/.elan/env
動作確認
以下のコマンドで、Lean4が正しくインストールされたか確認します。
lean --version
lakeの動作確認
Lean4のビルドツールであるlakeの動作確認も行います。
lake --version
Lean4のプロジェクト作成
Lean4のプロジェクトを作成するには、以下のコマンドを実行します。
lake new my_lean4_project
cd my_lean4_project
これで、Lean4のセットアップが完了しました。あとは、プロジェクト内でLean4のコードを書き始めることができます。
サンプルコードの実行
以下のような簡単なLean4のコードを書いてみましょう。
def main : IO Unit :=
IO.println "Hello, Lean4!"
このコードをMain.leanというファイルに保存し、以下のコマンドで実行します。
lake run
実行時に "Hello, Lean4!" と表示されれば、セットアップは成功です。
まとめ
この記事では、Lean4のセットアップ方法について説明しました。Lean4を使用して、形式的検証や定理証明を始める準備が整いました。今後は、Lean4のドキュメントやチュートリアルを参考にしながら、さらに深く学んでいきましょう。