Linux全般にLean 4をインストールする方法
ここでは、Linux全般にLeanをインストールする方法を説明します。(Debianとその派生ディストリビューションへのインストール方法はこちらのページをご覧ください。)
以下の全てのコマンドはターミナル内で入力してください。
-
Lean自体を動かすために必要なパッケージは少ないですが、
elanのインストールやlakeを使ったLeanプロジェクト作成にはgitとcurlが必要です。したがって、まずはgitとcurlをインストールしてください。 -
次は、
elanと呼ばれる小さなツールをインストールします。このツールは、Leanをアップデートしたり、Leanプロジェクトの要求に応じたバージョンのLeanを提供したりします。コマンドの実行中に質問が表示されたらEnterキーを押してください。elanは$HOME/.elanにインストールされ、$HOME/.profileに1行追加されます。curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -
VS Code、Emacs、Neovimの3つのエディタ上でLeanを使うことができます。おすすめのエディタはVisual Studio Code (VS Code)です。Leanにとって、VS Codeは最も完成度が高く、よくテストされたサポートを提供するエディタです。次の手順により、VS Codeがインストールされます。
- VS Codeをインストールします。
- VS Codeを起動します。
- スクリーンの左端のサイドバーにある拡張機能アイコン
(古いバージョンでは 
) をクリックし(あるいはShift-Ctrl-Xを押し)、leanproverと検索します。 lean4拡張機能(leanprover.lean4という一意の名前を持ちます)を選びます。- 「Install」をクリックします。(古いバージョンのVS Codeを使っている場合、インストール後に「reload」をクリックする必要があります。)
- Leanが動作していることを確認してください。例えば、ファイルに
test.leanと名前を付けて保存し、#eval 1+1と入力してみてください。#eval 1+1の下部に緑色の線が表示され、そこにマウスを乗せたときに2と表示されたらインストール成功です。
他の選択肢として、Emacsとlean4-modeを使ってLeanを扱うこともできます。また、Neovimとlean.nvim extensionを使うことも可能です。