MacOS(Intel Mac)にLean 4をインストールする方法 - 詳細な手順
ここでは、MacOS(Intel Mac)にLean 4をインストールする、より詳細な手順を説明します。簡単で高速なインストール手順もありますが、この手順を利用するには実行されるコマンドやbashスクリプトを信頼する必要があります。
Leanを使うにあたり、まずLeanと、Leanを扱う機能を持つエディタをセットアップする必要があります。Leanを直接インストールする代わりに、Leanをアップデートしたり、Leanプロジェクトの要求に応じたバージョンのLeanを提供する、elanという名前の小さなプログラム(バージョンマネージャ)をインストールします。elanのインストールは全てのユーザに推奨されます。
elanとLeanのインストール
-
まだHomebrewをインストールしていない場合は、Homebrewをインストールします。
-
ターミナルウィンドウ内で次のコマンドを実行し、
elanをインストールします。brew install elan-initHomebrewに
leanという名前のformulaがありますが、これはバージョン固定のLeanをインストールすることに注意してください。この場合、elanによってLeanプロジェクトの要求に応じたバージョンのLeanが提供されることはありません。このformulaの使用は推奨されません。 -
次のコマンドを実行し、
leanの最新のstableバージョンをインストールします。elan toolchain install stable次のコマンドを使うと、今インストールしたLeanのバージョンをデフォルトバージョンに設定することができます。Leanプロジェクトの外部でLeanを使う際は、このデフォルトバージョンが提供されます。
elan default stable
エディタのインストールと設定
VS Code、Emacs、Neovimの3つのエディタ上でLeanを使うことができます。このドキュメントでは、VS Codeを使う方法を説明します。VS CodeはLeanに最も良好なサポートを提供します。Emacsを使う場合は、https://github.com/leanprover/lean4-modeをご覧ください。Neovimを使う場合は、https://github.com/Julian/lean.nvimをご覧ください。
- VS Codeをインストールします。
- VS Codeを起動します。
- スクリーンの左端のサイドバーにある拡張機能アイコン
(古いバージョンでは 
) をクリックし(あるいは⇧ Shift⌘ CommandXを押し)、leanproverと検索します。 lean4拡張機能(leanprover.lean4という一意の名前を持ちます)を選びます。- 「Install」をクリックします。(古いバージョンのVS Codeを使っている場合、インストール後に「reload」をクリックする必要があります。)
- Leanが動作していることを確認してください。例えば、ファイルに
test.leanと名前を付けて保存し、#eval 1+1と入力してみてください。#eval 1+1の下部に緑色の線が表示され、そこにマウスを乗せたときに2と表示されたらインストール成功です。