MacOSにLean 4をインストールする方法 - 簡単な手順

ここでは、MacOSにLeanをインストールする手順を説明します。

特に、M1 Mac / Apple Siliconの場合はやや複雑な手順を含みます。行き詰まった場合は、Lean - Zulip Chat (英語)またはlean-ja Discussions (日本語)で助けを求めてください。

注意とお願い(必ずお読みください)

以下では翻訳元に従い、Intel Macについては curl を利用する方法、M1 Mac / Apple Siliconについては複雑な手順を紹介していますが、翻訳元ならびに以下の記述はLean 3のときの情報から更新されていない可能性があり、Lean 4ではMacOSにおいてもVS Codeのlean4拡張機能にelanとLeanをインストールしてもらう簡単な方法(以下「Quickstartインストール」とする)が有効である可能性が示唆されています1。少なくとも、M1 Mac・M2 Macにおいては、Windowsと同様にQuickstartインストールが有効だったという報告があります。以上の状況を鑑みて、暫定的ではありますが、この資料では次のようにインストール手順を案内いたします。

  1. 簡単な方法でのインストールを希望する場合:
    Quickstartインストールを試すことを推奨いたします。

  2. より確実な方法でのインストールを希望する場合、またはQuickstartインストールが上手くいかなかった場合:
    このページの以下に示すインストール方法を推奨いたします。

MacOSにおいて、Quickstartインストールに成功あるいは失敗した場合、プロセッサあるいはチップの情報付きでGitHubのIssuesに報告して頂けると幸いです。情報が集まり次第、このページの内容も更新いたします。

Intel Mac

ここでは簡単で高速なインストール方法を紹介します。この手順を使うと、Lean、そのサポートツールである elan と lake、コードエディタVS CodeとそのLeanプラグインがインストールされます。

ただし、この方法はbashスクリプトによるsudoコマンドの実行を含むほか、インストールプロセスの細部が分からないというデメリットもあります。ここで紹介するコマンドや、コマンド内で実行されるシェルスクリプトが信頼できない場合は、この方法は使わず、代わりにより詳細なインストール手順をご覧ください。

ターミナルを開き、次のように入力して実行すると、簡単で高速にLean 4をインストールすることができます。

/bin/bash -c "$(curl -fsSL https://raw.githubusercontent.com/leanprover-community/mathlib4/master/scripts/install_macos.sh)" && source ~/.profile

M1 Mac / Apple Silicon

GitHub ActionsがまだApple ARM上でのビルドをサポートしていないため、Leanのインストール方法はやや複雑です。

具体的には、Leanのバージョンマネージャ elan は、通常の方法でインストールされた場合、インストールされたデバイス上のLeanバイナリをフェッチすることができません。

以下の手順はFedor Pavutnitskiy氏からの引用です。この手順を使うと、Rosetta を通して elan をインストールすることができます。

  1. 新しいターミナルウィンドウを開き、次のコマンドを実行します。XCode Command Line ToolsとRosetta 2がインストールされます。

    xcode-select --install
softwareupdate --install-rosetta

  2. x86版のHomebrewをインストールします。最も簡単な方法は、Rosetta 2を使ってx86が動作するシェルを立ち上げる方法です。まず、次のコマンドを実行し、x86が動作するシェルを立ち上げます。

    arch -x86_64 zsh

    以降のコマンドはこのx86が動作するシェルウィンドウの中で実行しますが、一度インストールが完了すれば、インストールされたツールはどのシェルでも動作するはずです。

  3. 次のコマンドを実行し、x86版のHomebrewをインストールします。これは /opt ではなく /usr/local に自動的にインストールされるはずです。

    /bin/bash -c "$(curl -fsSL https://raw.githubusercontent.com/Homebrew/install/HEAD/install.sh)"

  4. 今インストールしたバージョンの brew を使って、MacOSへの詳細なインストール手順と同様の次のコマンドを実行します。

    /usr/local/bin/brew install elan-init
elan toolchain install stable
elan default stable

  5. 次のコマンドを実行してVisual Studio CodeとそのLean拡張機能をインストールします。コマンド内で brew のバージョンが指定されていませんが、x86版の brew でもARM版の brew でも正常に動作するはずです。

    brew install --cask visual-studio-code && code --install-extension leanprover.lean4

Zulipスレッド (英語)にインストール過程の詳細とアドバイスが書かれています。問題が起きたときは、遠慮なく助けを求めてください。

新しいターミナルを開いたときに command not found エラーが発生した場合は、MacOSからログアウトして再度ログインすれば解決するはずです。

参考資料