Leanのインストール方法・elanとLakeの使い方

by aconite

このドキュメントは有志による非公式資料です。

Leanのインストール方法と、LeanのバージョンマネージャelanとパッケージマネージャLakeの使い方を紹介します。Leanやelanをアップデートする方法、Mathlibを使用するLeanプロジェクトを作る方法を含みます。

この資料はMIT Licenseに基づいてLean Community ページの一部を翻訳した派生成果物と、Apache License 2.0に基づいてLean Manualの一部を翻訳した派生成果物を含みます。

この資料のソースはGitHubリポジトリから入手可能です。また、ページ右上端のGitHubマークを押してGitHubリポジトリに移動することもできます。この資料の全ページとソースはApache License 2.0の下で公開されています。

誤字脱字、内容の誤りの指摘、フォークからのPull Request、フォークによる資料の改変等は歓迎いたします。基本的に、ご指摘はGitHubリポジトリのIssuesで受け付けます。

各ページの下部に参考資料の一覧を掲載しています。主な参考資料はLean CommunityのInstallationカテゴリです。主な翻訳元には「翻訳元」と明記しています。また、信頼性の目安となることを想定し、ドメイン名と筆者情報に依って公式情報と判断したものには「公式」と明記していますが、本資料は「公式」と明記した資料が公式情報であることも、「公式」と明記していない資料が非公式情報であることも保証いたしません。

この資料を参考にしてMacOSへのLeanのインストールを希望される方は、節「注意とお願い」を必ずお読みください。

mdBook付属の検索機能に関して、今のところ日本語検索は非対応です。お手数ですがページ内検索をご活用ください。

英語資料の翻訳に際して、機械翻訳サービスDeepL翻訳を参考にしました。

Leanのインストール方法

以下の各OSについてインストール手順を紹介します。

• Debian/Ubuntu
• Linux全般
• MacOS
• Windows

インストール不要のオンラインバージョン、Lean 4 Webもあります。

また、GitpodやGitHub codespacesを使うことで、インストールすることなくクラウド上でLeanを使ってみることもできます。例えば、GitPod上で練習問題を解きながら、テキストMathematics in Leanを読むことができます。Gitpodを使うには、GitHubかGitLabにログインする必要があることに注意してください。

インストールに行き詰まった場合は、Lean - Zulip Chat (英語)またはlean-ja Discussions (日本語)で助けを求めることを検討してください。

参考資料

• Get started with Lean - Lean Community : 翻訳元、公式。
• プログラミング言語Lean 4の現状 - 檜山正幸のキマイラ飼育記 (はてなBlog) : 檜山正幸さんによるLean 4まとめ記事です。curl によるelan・Leanのインストール方法のほか、Leanプロジェクト・パッケージについても詳説されています。
• 関数型言語”兼”定理証明支援系Leanの環境構築 - Zenn : denjiryさんによるLeanの環境構築記事です。curl によるelan・Leanのインストール方法、elanとLakeの紹介のほか、エディタとしてEmacsを使う際の設定方法が紹介されています。

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

ここでは、Debianから派生したLinuxディストリビューション(Debian、Ubuntu、LMDEなど)にLeanをインストールする簡単で高速な手順を説明します。この手順を使うと、Lean、そのサポートツールであるelanとLake、コードエディタVS CodeとそのLeanプラグイン、そしてcurlやgitのような既にインストールされている可能性のある依存関係パッケージがインストールされます。

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

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

wget -q https://raw.githubusercontent.com/leanprover-community/mathlib4/master/scripts/install_debian.sh && bash install_debian.sh ; rm -f install_debian.sh && source ~/.profile

参考資料

• How to install Lean 4 on Debian/Ubuntu - Lean Community : 翻訳元、公式。

Debian/UbuntuにLean 4をインストールする方法 - 詳細な手順

ここでは、Debianから派生したLinuxディストリビューション(Debian、Ubuntu、LMDEなど)にLean 4をインストールする、より詳細な手順を説明します。簡単で高速なインストール手順もありますが、この手順を利用するには実行されるコマンドやbashスクリプトを信頼する必要があります。

厳密にいえば、ここで紹介する手順もシェルスクリプトの実行を含みます。elan_initを読むことで、以下のインストール手順のより細部を知ることができます。

• Lean自体を動かすために必要なパッケージは少ないですが、elan のインストールや lake を使ったLeanプロジェクト作成には git と curl が必要です。したがって、まずは git と curl をインストールします。

  sudo apt install 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がインストールされます。

  wget -O code.deb https://go.microsoft.com/fwlink/?LinkID=760868
  sudo apt install ./code.deb
  rm code.deb
  code --install-extension leanprover.lean4
  

以上の手順が終わったら、VS Codeを開き、Leanが動作していることを確認してください。例えば、ファイルに test.lean と名前を付けて保存し、#eval 1+1 と入力してみてください。#eval 1+1 の下部に緑色の線が表示され、そこにマウスを乗せたときに 2 と表示されたらインストール成功です。

他の選択肢として、Emacsとlean4-modeを使ってLeanを扱うこともできます。また、Neovimとlean.nvim extensionを使うことも可能です。

参考資料

• Controlled installation of Lean 4 on Debian/Ubuntu - Lean Community : 翻訳元、公式。

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がインストールされます。

  1. VS Codeをインストールします。
  2. VS Codeを起動します。
  3. スクリーンの左端のサイドバーにある拡張機能アイコン (古いバージョンでは ) をクリックし(あるいはShift-Ctrl-Xを押し)、leanprover と検索します。
  4. lean4 拡張機能(leanprover.lean4 という一意の名前を持ちます)を選びます。
  5. 「Install」をクリックします。(古いバージョンのVS Codeを使っている場合、インストール後に「reload」をクリックする必要があります。)
  6. Leanが動作していることを確認してください。例えば、ファイルに test.lean と名前を付けて保存し、#eval 1+1 と入力してみてください。#eval 1+1 の下部に緑色の線が表示され、そこにマウスを乗せたときに 2 と表示されたらインストール成功です。

他の選択肢として、Emacsとlean4-modeを使ってLeanを扱うこともできます。また、Neovimとlean.nvim extensionを使うことも可能です。

参考資料

• Installing Lean 4 on Linux - Lean Community : 翻訳元、公式。

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インストール」とする)が有効である可能性が示唆されています¹。少なくとも、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からログアウトして再度ログインすれば解決するはずです。

参考資料

• How to install Lean 4 on MacOS - Lean Community : 翻訳元、公式。

MacOS(Intel Mac)にLean 4をインストールする方法 - 詳細な手順

ここでは、MacOS(Intel Mac)にLean 4をインストールする、より詳細な手順を説明します。簡単で高速なインストール手順もありますが、この手順を利用するには実行されるコマンドやbashスクリプトを信頼する必要があります。

Leanを使うにあたり、まずLeanと、Leanを扱う機能を持つエディタをセットアップする必要があります。Leanを直接インストールする代わりに、Leanをアップデートしたり、Leanプロジェクトの要求に応じたバージョンのLeanを提供する、elanという名前の小さなプログラム(バージョンマネージャ)をインストールします。elanのインストールは全てのユーザに推奨されます。

elanとLeanのインストール

1. まだHomebrewをインストールしていない場合は、Homebrewをインストールします。

2. ターミナルウィンドウ内で次のコマンドを実行し、elan をインストールします。

   brew install elan-init
   

   Homebrewに lean という名前のformulaがありますが、これはバージョン固定のLeanをインストールすることに注意してください。この場合、elan によってLeanプロジェクトの要求に応じたバージョンのLeanが提供されることはありません。このformulaの使用は推奨されません。

3. 次のコマンドを実行し、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をご覧ください。

1. VS Codeをインストールします。
2. VS Codeを起動します。
3. スクリーンの左端のサイドバーにある拡張機能アイコン (古いバージョンでは ) をクリックし(あるいは⇧ Shift⌘ CommandXを押し)、leanprover と検索します。
4. lean4 拡張機能(leanprover.lean4 という一意の名前を持ちます)を選びます。
5. 「Install」をクリックします。(古いバージョンのVS Codeを使っている場合、インストール後に「reload」をクリックする必要があります。)
6. Leanが動作していることを確認してください。例えば、ファイルに test.lean と名前を付けて保存し、#eval 1+1 と入力してみてください。#eval 1+1 の下部に緑色の線が表示され、そこにマウスを乗せたときに 2 と表示されたらインストール成功です。

参考資料

• Controlled installation of Lean 4 on MacOS - Lean Community : 翻訳元、公式。

WindowsにLean 4をインストールする方法 - 簡単な説明

ここでは、VS CodeでLeanを扱えるようにし、そしてLeanをセットアップする方法を簡単に説明します。このインストール手順では、Lakeを使ってLeanプロジェクトを作るために必要な git がインストールされないことに注意してください。git のインストール方法を知りたい場合や、詳細な説明を読みたい場合は、このページをご覧ください。

1. まず、VS Codeをインストールします。

2. VS Codeを起動し、lean4 拡張機能をインストールします。

   

3. 画面上部にある File メニューを開き、New text file を選びます(ショートカット: Ctrl+N)。Untitled-1 とラベルされた新しいウィンドウが開きます。新しいウィンドウには Select a language と表示されます。この表示をクリックし、lean4 を選びます。画面右下に次のようなポップアップが表示されます。

   

   「Install Lean using Elan」ボタンをクリックします。VS Code 内でターミナルウィンドウが立ち上がり、インストールが始まります。ウィンドウ内には次のような出力を含むテキストが表示されるはずです。

   info: syncing channel updates for 'nightly'
   info: latest update on nightly, lean version nightly-2023-06-27
   info: downloading component 'lean'
   

   もし Failed to start 'lean' language server と書かれたポップアップが表示されなかった場合、elan が既にインストールされている可能性があります。その場合、コマンド elan default leanprover/lean4:nightly を実行し、デフォルトツールチェインがLean 4であることを確定させ、それから再びVS Code内でテキストファイルを開いてください。この操作を行わなかった場合、次のステップで失敗する可能性があります。

4. インストールが終わったら、Lean言語サーバーが自動的に立ち上がり、シンタックスハイライトが有効になり、「Lean Infoview」ウィンドウが右側に表示されます。以上を確認したら、次のコードをLeanファイルにペーストします。

   #eval Lean.versionString
   

   このコードの末尾にカーソルを合わせると、「Lean Infoview」ウィンドウにインストールされたLeanのバージョンが表示されます。

   

この表示が確認できたら、セットアップ成功です！

参考資料

• Setting Up Lean - Lean Manual : 翻訳元、公式。
• 定理証明支援系Lean 4導入手順【VOICEROID解説】 - YouTube : ぐにらちさんによる、上記インストール手順の解説動画です。

WindowsにLean 4をインストールする方法 - 詳細な説明

ここでは、WindowsにLeanをインストールする方法を説明します。

Leanを使うにあたり、まずLeanと、Leanを扱う機能を持つエディタをセットアップする必要があります。Leanを直接インストールする代わりに、Leanをアップデートしたり、Leanプロジェクトの要求に応じたバージョンのLeanを提供する、elanという名前の小さなプログラム(バージョンマネージャ)をインストールします。elanのインストールは全てのユーザに推奨されます。

Visual Studio Codeのインストール

全てのWindowsユーザーに対して、エディタ Visual Studio Code(VS Code) を使ってLeanを扱うことをお勧めします。https://code.visualstudio.com/downloadから VS Code をインストールすることができます。

gitのインストール

Lean 4 プロジェクト間の依存関係は、gitリポジトリへのポインタを介して実装されています。したがって、Leanプロジェクトを作るには、お使いのコンピュータにgitをインストールする必要があります。

既にgitをインストールしてある場合は、このステップを飛ばすことができます。

もしgitがインストールされていないなら、Git for Windowsをインストールすることをお勧めします。インストール中、多くの質問を受けますが、デフォルトエディタに関する質問以外はデフォルトの選択肢を選ぶことをお勧めします。デフォルトエディタに関する質問では、デフォルト選択肢 vi の代わりに Visual Studio Code を選ぶことをお勧めします。

編集するテキストファイルの改行コードを変えないようにするために(改行コードをLFで統一するために)、コマンド git config --global core.autocrlf input を実行することをお勧めします。

VS Codeにlean4拡張機能をインストール

VS Code を開き、画面左端の「アクティビティバー」の中にある「拡張機能」アイコン をクリックします。

検索ボックスが表示されるので、lean4 と入力し、検索結果に表示される lean4 拡張機能を選択します。「Install」ボタンをクリックすると拡張機能がインストールされます。

elanとLeanのセットアップ

elan と lean のセットアップについては、VS Code の lean4 拡張機能に任せることも、手動でセットアップすることもできます。lean4 拡張機能にセットアップを任せることをお勧めしますが、以下では両方の手順を説明します。

lean4拡張機能にelanとLeanをインストールしてもらう方法

画面上部にある File メニューを開き、New text file を選びます。Untitled-1 とラベルされた新しいウィンドウが開きます。

新しいウィンドウには Select a language と表示されます。この表示をクリックし、lean4 を選びます。(画面右下端に表示される Plain text をクリックして言語を選択することもできます。また、Ctrl+Shift+P を押して「コマンドパレット」を開き、そこで Change language mode を選んで言語を選択することもできます。)

言語を lean4 に設定すると、画面右下端に、Failed to start 'lean' language server と書かれた、Install Lean using Elan ボタン付きのダイアログボックスが表示されます。

Install Lean using Elan ボタンをクリックします。そうすると、VS Code 内でターミナルウィンドウが立ち上がり、インストールが始まります。Lean のダウンロードとインストールには1分程度かかります。

インストールが終わったら、Untitled-1 ウィンドウに戻り、次のように入力します。

#eval 18 + 19

#eval の下に青い波線が引かれ、右側の Lean Infoview パネルに 37 が表示されたら、Lean 4のインストールは成功です！

手動でelanをインストールする方法

コマンドプロンプト(cmd)を開き、次のコマンドを実行します。

curl -O --location https://raw.githubusercontent.com/leanprover/elan/master/elan-init.ps1
powershell -ExecutionPolicy Bypass -f elan-init.ps1
del elan-init.ps1

あるいは、Git Bash を開き、次のコマンドを実行します。

curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh

どちらの方法でも、elan のインストールには1分程度かかります。インストールが終わったら、VS Code を開き、画面上部にある File メニューを開き、New text file を選びます。新しいテキストが開かれたら、Select a language と書かれた部分をクリックし、lean4 を選びます。(あるいは、新しいテキストを .lean 拡張子で保存します。)

それから、次のように入力して、Leanがユーザーの入力に反応することを確認してください。

#eval 18 + 19

以上でインストールは完了です！

参考資料

• Installing Lean 4 on Windows - Lean Community : 翻訳元、公式。

elan: Leanバージョンマネージャ

elanは、Leanをインストール・アップデートしたり、Leanプロジェクトの要求に応じたバージョンのLeanを提供したりする、Leanの小さなバージョンマネージャです。

elanのインストール方法

インストールページに従ってLeanがインストールされていれば、elanもインストールされているはずです。手動でインストールしたい場合はここに挙げる方法を使ってください。

手動でインストールする場合は、ターミナル内で次のコマンドを実行します。

Linux/macOS/Cygwin/MSYS2/git bash/...:

curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh

Windows:

curl -O --location https://raw.githubusercontent.com/leanprover/elan/master/elan-init.ps1
powershell -ExecutionPolicy Bypass -f elan-init.ps1
del elan-init.ps1

あるいは、最新のリリースをダウンロードし、解凍し、その中のインストールプログラムを実行させてelanをインストールすることもできます。

ここで説明したインストール方法を実行した場合、インストーラは elan、lean、lake のバイナリを ~/.elan/bin にインストールすること、~/.profile を更新して ~/.elan/bin をPATH環境変数に加えることを説明します。~/.profile の更新により、次回以降シェルを起動した際は自動で ~/.elan/bin にパスが通りますが、現在のシェルにおいてパスを通したい場合はコマンド source ~/.elan/env を実行してください。

elanのフォーク元

elanはRustのツールチェイン・インストーラrustupのフォークです。基本的に、RustとLeanを比較すると、rustup は elan に、cargo は lake に相当します。

elanに関する用語

• toolchain(ツールチェーン) : 特定のバージョンのLean一式のことです。
• channel(チャンネル) : ツールチェーンの系統のことです。Lean4には nightly と stable の2つのチャンネルがあります。

参考資料

• leanprover/elan: A Lean version manager - GitHub : 翻訳元、公式。上記の情報に加え、HomebrewやNixを使ったインストール方法や、elanのビルド方法が紹介されています。

Leanとelanのアップデート

以下のコマンドは全てターミナル上で実行するものです。また、# はコメントを表します(rootユーザでのコマンドの行頭の記号を表すものではありません)。

elanのヘルプ情報を表示する

次のコマンドを実行すると、elanのヘルプ情報(使い方等)を表示することができます。

elan -h

elanのアップデート

次のコマンドを実行すると、elan自体をアップデートすることができます。Windowsをお使いの場合、VS Codeが起動していない状態でこのコマンドを実行してください。¹

elan self update

次のコマンドを実行すると、elanのバージョンが表示されます。

elan -V

Leanのアップデート

次のコマンドを実行すると、elanとLeanの両方をアップデートすることができます。

elan update

次のコマンドを実行すると、インストール済みのツールチェーンの一覧と現在アクティブなツールチェーンを表示します。

elan show

デフォルトツールチェーンの変更

次のコマンドを実行すると、指定したツールチェーンをインストールし、そのツールチェーンをデフォルトに設定します。

# elan default <ツールチェーン名>
elan default leanprover/lean4:nightly
# 例えば、stableチャンネルのツールチェーンに切り替えたいときは次を実行する:
# elan default leanprover/lean4:stable

参考資料

• Extended Setup Notes - Lean Manual : 翻訳元、公式。
• Channels - The rustup book : Rust公式。
• Toolchains - The rustup book : Rust公式。
• プログラミング言語Lean 4の現状 - 檜山正幸のキマイラ飼育記 (はてなBlog) : 檜山正幸さんによるLean 4まとめ記事です。上記の内容に加え、ツールチェーン名の命名パターンが詳説されているほか、具体的なコマンドの実行例が掲載されています。

Lake: Leanパッケージマネージャ編

Lake(Lean Make)はLean 4のためのビルドシステム兼パッケージマネージャです。Lakeを使うと、Leanパッケージを作ることができ、そしてLeanパッケージの設定をLean自体で書くことができます。Leanパッケージの設定はパッケージのルートディレクトリの lakefile.lean というファイルに保存されます。

lakefile.lean は、パッケージの基本設定を定義する package 宣言を含みます。また、通常、Leanライブラリやバイナリ実行ファイルなどのためのビルド設定と、コマンドラインでコマンド lake script run によって実行されるLeanスクリプト宣言も含みます。

この章では、Lakeのパッケージマネージャとしての側面に焦点を当てます。基本的に、パッケージの作成・管理にはGitが必要です。まだGitをインストールしていない場合は、先にGitのインストールを済ませてください。

Lakeのインストール方法

Lakeはlean4リポジトリの一部として、つまりelanツールチェーンの一部として、Leanの公式リリースに付属しています。したがって、もしお使いのコンピュータに最近のLean 4 nightlyがインストールされていれば、Lakeもインストールされているはずです。

Lakeに関する用語集

ここではパッケージに関する用語に絞って紹介します。

• project(プロジェクト)は、Lakeによって作られる、適切な構造を持ったGitリポジトリです。例えば、コマンド lake new foo を実行すると、次のようなファイル構造を持つフォルダ foo が作られます。これが初期化されたプロジェクトです。

  └─foo
      ├─.git
      │   └─(省略)
      ├─.gitignore
      ├─lakefile.lean  # パッケージ設定ファイル
      ├─lean-toolchain # このプロジェクトで使うLeanのバージョンを指定する
      ├─Main.lean      # 主にバイナリ実行ファイルのビルド元として使われる
      └─Foo.lean       # プロジェクト内の全モジュールを一括インポート(``import Foo``)するために使われる
  

  基本的に、プロジェクトのルートには更にフォルダ Foo が作られ、その中に個別のleanファイルが置かれます。したがって、プロジェクトの基本的な構造は次のようになります。

  └─foo
      ├─.git
      │   └─(省略)
      ├─Foo
      │   ├─A.lean     # 個別のLeanファイル。``import Foo.A`` を使ってインポートする
      |   (省略)
      ├─.gitignore
      ├─lakefile.lean
      ├─lean-toolchain
      ├─Main.lean
      └─Foo.lean
  

• package(パッケージ)は、プロジェクトのスナップショットです。Lakeにおける配布コードの基本単位とも説明されます。ただし、公式情報においてもプロジェクトとパッケージの間に明確な区別はありません。以降、このページでは統一してパッケージという用語を使います。パッケージはローカルのファイルシステムから読み込むことも、Gitを経由してWebからダウンロードすることもできます。パッケージの lakefile.lean の中の package 宣言では、パッケージに名前を付け、基本的なプロパティを定義します。

• lakefileはパッケージの設定を行うLeanファイルです。lakefileはパッケージ内のコードを読む・編集する・ビルドする・実行する方法を定義し、さらにこのパッケージにおける被依存パッケージを指定します。

• dependency(被依存パッケージ)は、あるパッケージに依存されるパッケージのことで、dependent(依存パッケージ)は、その被依存パッケージに依存するパッケージのことです。

• module(モジュール)はLakeのビルドシステムが認識できる最小のコード単位です。モジュールは一般的にLeanのソースファイル(.lean)とバイナリライブラリ(.olean と .ilean)で構成されます。precompileModules がオンの場合はシステム共有ライブラリもモジュールの構成要素となります。モジュールは他のモジュール内のコードを使用するためにそのモジュールをインポートする(import <module_name>)ことができ、Lakeは主にこのプロセスを容易にするために存在します。

• workspace(ワークスペース)はLakeにおける最も大きな組織単位です。ワークスペースは、パッケージ、その被依存パッケージ、Lakeの環境をまとめたものです。全てのパッケージはワークスペースのルートとして機能し、ワークスペースはルートから設定を派生させます。

参考資料

• leanprover/lake: Lean 4 build system and package manager with configuration files written in Lean. : 翻訳元、公式。README.md に詳細な情報が書かれています。
• Extended Setup Notes - Lean Manual : 公式。
• プログラミング言語Lean 4の現状 - 檜山正幸のキマイラ飼育記 (はてなBlog) : 檜山正幸さんによるLean 4まとめ記事です。プロジェクトとパッケージに関する記述を参考にしました。

既存のLeanプロジェクトの使い方

既存のLeanプロジェクトの使い方を説明します。ここでは、Mathematics in Leanを例にとります。まずターミナルを開きます。

• もしelanとLeanのインストールに使ったターミナルを閉じずに使い続けている場合、LeanやelanやLake等にパスを通すために次のコマンドを実行してください。コマンドはOSに応じて変わります。

  source ~/.profile
  

  または

  source ~/.bash_profile
  

• cd コマンドを使って使いたいパッケージを置きたいフォルダに移動します。Leanプロジェクト用のサブフォルダは自動的に作られるため、手動で作る必要はありません。

• 移動先のフォルダ上で次のコマンドを実行し、Leanプロジェクト「Mathematics in Lean」をクローンします。

  git clone https://github.com/leanprover-community/mathematics_in_lean.git
  

• 次のコマンドを実行し、クローンしたプロジェクトのルートディレクトリに移動します。

  cd mathematics_in_lean
  

• 次のコマンドを実行し、キャッシュされたビルド済みファイルをダウンロードします。(このコマンドは現在、mathlib4 をインポートするプロジェクト内でしか機能しません)

  lake exe cache get
  

• アプリケーションメニューから、あるいはコマンド code . を実行して、VS Codeを起動します。(Mac OSユーザーがコマンドラインからVS Codeを立ち上げるためには、もう1ステップ作業する必要があります。)

• VS Codeを起動したら、画面上部にある File メニューを開き、Open folder(Macの場合は Open)をクリックし、mathematics_in_lean フォルダを選択します(mathematics_in_lean フォルダ内のサブフォルダを選ばないように注意してください)。

• 左端のサイドバー内のファイルエクスプローラーを使ってサブフォルダ MIL の中を探し、開きたいLeanファイルを開きます。この本の練習問題に取り組む方法はMIL instructionsに書かれています。

参考資料

• Lean projects - Lean Community : 翻訳元、公式。
• leanprover-community/mathlib4: The math library of Lean 4 : 公式。
• leanprover/lake: Lean 4 build system and package manager with configuration files written in Lean. : 公式。README.md に詳細な情報が書かれています。

おすすめのLeanプロジェクト教材

• lean-math-workshop (日本語) : 『数学系のためのLean勉強会』のために作成された教材です。Leanの基本的な使い方を学ぶBasic編と、代数・解析・圏論の各分野における定理を実際に証明するAdvanced編に分かれています。
  Advanced編で証明する定理には「群の準同型定理」「閉区間[0, 1]のコンパクト性」などが含まれます。

• Mathematics in Lean (英語) : 論理・集合から測度論・微積分までの数学の定理を実際に形式証明しながらLean 4を学ぶテキストです。

• The mechanics of proof (英語) : 計算による等式や不等式の証明から始まり、数論や代数分野の高校数学程度の問題について、形式的な証明の書き方を学べるテキストです。
  cancelなど、Index of Lean tacticsページにおいて先頭に"*"が付けられたタクティクは、Leanの標準ライブラリやMathlibには存在しない、この教材独自のタクティクであることに注意してください。

Leanプロジェクトの作り方

前提として、Git がインストールされていることをご確認ください。

Mathlib4の使用を前提としないLeanプロジェクトの新規作成方法

Mathlib4の使用を前提としないLeanプロジェクト my_project を新規作成する手順を説明します。まずターミナルを開きます。

• 次のコマンドを実行し、elan・lean・lake をアップデートします。

  elan update
  

• cd コマンドを使って my_project を作りたいフォルダに移動します。

• 次のコマンドのいずれかを実行します(どちらでも結果は同じです)。新しいLeanプロジェクトが作成されます。

  lake new my_project
  

  あるいは

  mkdir my_project
  cd my_project
  lake init my_project
  

Mathlib4を使うLeanプロジェクトの新規作成方法

Mathlib4を使うLeanプロジェクト my_project を新規作成する手順を説明します。まずターミナルを開きます。

• 次のコマンドを実行し、elan・lean・lake をアップデートします。

  elan update
  

• cd コマンドを使って my_project を作りたいフォルダに移動します。

• 次のコマンドを実行します。Mathlib4への依存関係が設定された新しいLeanプロジェクトが作成されます。

  lake new my_project math
  

• 次のコマンドを実行し、作成したLeanプロジェクト内に移動します。

  cd my_project
  

• 次のコマンドを実行し、Mathlib4を含む被依存パッケージをダウンロードします。

  lake update
  

• 次のコマンドを実行し、Mathlib4のキャッシュされたビルド済ファイルをダウンロードします。

  lake exe cache get
  

• 次のコマンドを実行し、Leanファイルを置くためのサブディレクトリ MyProject を作成します。

  mkdir MyProject
  

• VS Codeを開き、画面上部にある File メニューを開き、Open folder(Macの場合は Open)をクリックし、my_project フォルダ(MyProject フォルダではありません)を選択します。

これでMathlib4を使うLeanプロジェクト my_project の新規作成は完了です。以降、プロジェクトのLeanファイル(拡張子 .lean)は MyProject フォルダかそのサブフォルダ上に作成してください。

Leanプロジェクトが正常に作成され、Mathlib4内のモジュールがインポートできることを確認するには、次のような方法があります:

• 画面左端のサイドバーのファイルエクスプローラーを開き、MyProject フォルダにカーソルを合わせて右クリックし、New File をクリックし、test.lean という名前のファイルを作成します。

• VS Code上で test.lean を開き、ファイルに次のように入力します:

  import Mathlib.Topology.Basic
  
  #check TopologicalSpace
  

• #check TopologicalSpace にマウスカーソルを乗せ、VS Codeの右側の「Lean Infoview」に次のように表示されたら確認完了です。

  TopologicalSpace.{u} (α : Type u) : Type u
  

自作Leanファイル内で他の自作Leanファイルをインポートすることもできます。例えば、my_project/MyProject/Definitions.lean と my_project/MyProject/Lemmas.lean が存在する場合、Lemmas.lean の先頭に次のように書くことで、Definitions.lean の内容が利用可能になります。

import MyProject.Definitions

何らかの理由で右側の「Lean Infoview」が消えてしまった場合は、Ctrl-Shift-Enter(MacOSの場合は Cmd-Shift-Enter)を押すことで「Lean Infoview」を復活させることができます。また、Ctrl-Shift-p(MacOSの場合は Cmd-Shift-p)を押し、コマンドを入力するテキストフィールドを表示させ、「lean doc」と入力しEnterを押すと、「Mathematics in Lean」や「Theorem Proving in Lean 4」といったドキュメントを読むことができます。

既存のプロジェクトにMathlib4への依存関係を追加する方法

現時点でMathlib4に依存していないLeanプロジェクト my_project にMathlib4への依存関係を追加する手順を説明します。

• my_project/lakefile.lean を開き、次の記述を追加します。

  require mathlib from git
    "https://github.com/leanprover-community/mathlib4"
  

  ブランチを指定することもできます。

  require mathlib from git
    "https://github.com/leanprover-community/mathlib4" @ "master"
  

  ハッシュ値を付けてパッケージバージョン(Gitコミット)を固定することもできます。

  require mathlib from git
    "https://github.com/leanprover-community/mathlib4" @
  "9efcb9508435caeb4281b14455f37b88f8ffc2e5"
  

• ターミナルを開き、フォルダ my_project に移動します。

• パッケージバージョンを固定しなかった場合、次のコマンドを実行し、my_project 内で使われるLeanのバージョンを最新のMathlib4内で使われるLeanのバージョンに合わせます。

  curl -L https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain
  

• 次のコマンドを実行し、Mathlib4を含む被依存パッケージをダウンロードします。

  lake update
  

• 次のコマンドを実行し、Mathlib4のキャッシュされたビルド済ファイルをダウンロードします。

  lake exe cache get
  

以上で、既存のプロジェクトからMathlib4への依存関係の追加は完了です。

Leanプロジェクト内で、被依存パッケージMathlib4をアップデートする方法

• ターミナルを開き、フォルダ my_project に移動します。

• 次のコマンドを実行し、my_project 内で使われるLeanのバージョンを最新のMathlib4内で使われるLeanのバージョンに合わせます。

  curl -L https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain
  

• 次のコマンドを実行し、Mathlib4を含む被依存パッケージをダウンロードします。

  lake update
  

• 次のコマンドを実行し、Mathlib4のキャッシュされたビルド済ファイルをダウンロードします。

  lake exe cache get
  

以上でMathlib4のアップデートは完了です。

参考資料

• Lean projects - Lean Community : 翻訳元、公式。
• Using mathlib4 as a dependency · leanprover-community/mathlib4 Wiki : 公式。
• leanprover/lake: Lean 4 build system and package manager with configuration files written in Lean. : 公式。README.md に詳細な情報が書かれています。
• プログラミング言語Lean 4の現状 - 檜山正幸のキマイラ飼育記 (はてなBlog) : 檜山正幸さんによるLean 4まとめ記事です。「Leanプロジェクト」と「Leanパッケージ」の節を参考にしました。
• Installation Help - Lean - Zuip Chat : Mario Carneiroさんのメッセージを参考にしました。

Lake: Leanビルドシステム編

Lake(Lean Make)はLean 4のためのビルドシステム兼パッケージマネージャです。Lakeを使うと、Leanパッケージを作ることができ、そしてLeanパッケージの設定をLean自体で書くことができます。Leanパッケージの設定はパッケージのルートディレクトリの lakefile.lean というファイルに保存されます。

lakefile.lean は、パッケージの基本設定を定義する package 宣言を含みます。また、通常、Leanライブラリやバイナリ実行ファイルなどのためのビルド設定と、コマンドラインでコマンド lake script run によって実行されるLeanスクリプト宣言も含みます。

この章では、Lakeのビルドシステムとしての側面に焦点を当てます。

(後日更新予定)

参考資料

leanprover/lake: Lean 4 build system and package manager with configuration files written in Lean. : 翻訳元、公式。README.md に詳細な情報が書かれています。

FAQ

Leanのインストール方法

Q. VSCodeで lean4 拡張機能をインストールしたいのですが、「lean4」で検索しても複数の拡張機能がヒットします。どれをインストールしたらいいですか？

A. Leanのインストール手順で紹介されている lean4 拡張機能は「leanprover.lean4」という一意の名前(Extension ID)を持ちます。「lean4」の代わりに「leanprover.lean4」で検索すれば拡張機能が1件だけヒットしますので、それをインストールしてください。

Q. elan・lean・lake のバイナリはどのフォルダにインストールされますか？

A. elan・lean・lake のバイナリは ~/.elan/bin($HOME/.elan/bin) にインストールされます。

Q. elan・lean・lake(以下、「lean 等」とする) へのパスは自動で通りますか？

A. 例えば、WindowsでQuickstartインストールを行った場合は環境変数に~/.elan/binが自動で追加されます。また、Debianでbashをお使いの環境でインストールを行った場合は、設定ファイル~/.profile(あるいは ~/.bash_profile) が自動で更新され、パスが通ります。zshをお使いの場合も設定ファイルが自動で更新されます。したがって、インストール後にターミナルを再起動すれば lean 等へのパスは通ります。

ターミナルを再起動したくない場合は、コマンド source ~/.elan/env を実行すれば現在のターミナルでパスが通ります。~/.elan/env の内容は次の通りです。

export PATH="$HOME/.elan/bin:$PATH"

しかし、ターミナル fish をお使いの場合は自動でパスが通らないことが報告されています。他のターミナルをお使いの場合も自動でパスが通らない可能性が考えられます。その際は、~/.elan/env の内容を参考にして各自設定ファイルを編集し、パスを通してください。

Lake: Leanパッケージマネージャ編

Q. lake new <project_name> を実行してもLeanプロジェクトが作られません。どうしたらいいですか？

A. まずはお使いのコンピュータに Git がインストールされていることを確認してください。

Q. Leanプロジェクトにおいて lake update を実行すると次のようなエラーが出ます。どうしたらいいですか？

error: .\lakefile.lean:x:x error: unknown attribute [defaultTarget]

A. lean のバージョンアップに伴い、属性 [defaultTarget] が [default_target] に変更されたようです。このエラーが出た場合、lake のバージョンが古い可能性があります。elan update で elan・lean・lake をアップデートしてからLeanプロジェクトを作り直すか、lakefile.lean 内の [defaultTarget] を [default_target] に置換してください。

Q. Mathlibを使うLeanプロジェクトにおいて、コンパイルエラーが発生します。どうしたらいいですか？

A. Mathlibの lean-toolchain が指定するLeanのバージョンと、Leanプロジェクトの lean-toolchain が指定するLeanのバージョンが食い違うことによるエラーの可能性があります。Mathlib4のバージョンを固定していない場合は、Leanプロジェクト内で、被依存パッケージMathlib4をアップデートする方法を実行すれば解決する可能性があります。

Q. Mathlibを使うLeanプロジェクト内のLeanファイルを開きましたが、import がいつまで経っても終わりません。どうしたらいいですか？

A. キャッシュされたビルド済ファイルが正常にダウンロードされていない可能性があります。コマンド lake exe cache get が未実行ならこのコマンドを実行してください。lake exe cache get が実行済みならコマンド lake exe cache get! を試してみてください。lake exe cache get!はキャッシュされたビルド済ファイルのダウンロードをやり直します。

出典

Discordサーバー「code for math」の「#lean」チャンネル