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を使うことも可能です。