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についてインストール手順を紹介します。
インストール不要のオンラインバージョン、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
参考資料
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を使うことも可能です。
参考資料
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を使うことも可能です。
参考資料
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インストールが有効だったという報告があります。以上の状況を鑑みて、暫定的ではありますが、この資料では次のようにインストール手順を案内いたします。
-
簡単な方法でのインストールを希望する場合:
Quickstartインストールを試すことを推奨いたします。 -
より確実な方法でのインストールを希望する場合、または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
をインストールすることができます。
-
新しいターミナルウィンドウを開き、次のコマンドを実行します。XCode Command Line ToolsとRosetta 2がインストールされます。
xcode-select --install softwareupdate --install-rosetta
-
x86版のHomebrewをインストールします。最も簡単な方法は、Rosetta 2を使ってx86が動作するシェルを立ち上げる方法です。まず、次のコマンドを実行し、x86が動作するシェルを立ち上げます。
arch -x86_64 zsh
以降のコマンドはこのx86が動作するシェルウィンドウの中で実行しますが、一度インストールが完了すれば、インストールされたツールはどのシェルでも動作するはずです。
-
次のコマンドを実行し、x86版のHomebrewをインストールします。これは
/opt
ではなく/usr/local
に自動的にインストールされるはずです。/bin/bash -c "$(curl -fsSL https://raw.githubusercontent.com/Homebrew/install/HEAD/install.sh)"
-
今インストールしたバージョンの
brew
を使って、MacOSへの詳細なインストール手順と同様の次のコマンドを実行します。/usr/local/bin/brew install elan-init elan toolchain install stable elan default stable
-
次のコマンドを実行して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からログアウトして再度ログインすれば解決するはずです。
参考資料
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-init
Homebrewに
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
と表示されたらインストール成功です。
参考資料
WindowsにLean 4をインストールする方法 - 簡単な説明
ここでは、VS CodeでLeanを扱えるようにし、そしてLeanをセットアップする方法を簡単に説明します。このインストール手順では、Lakeを使ってLeanプロジェクトを作るために必要な git
がインストールされないことに注意してください。git
のインストール方法を知りたい場合や、詳細な説明を読みたい場合は、このページをご覧ください。
-
まず、VS Codeをインストールします。
-
VS Codeを起動し、
lean4
拡張機能をインストールします。 -
画面上部にある
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内でテキストファイルを開いてください。この操作を行わなかった場合、次のステップで失敗する可能性があります。 -
インストールが終わったら、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
以上でインストールは完了です!
参考資料
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が起動していない状態でこのコマンドを実行してください。1
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まとめ記事です。上記の内容に加え、ツールチェーン名の命名パターンが詳説されているほか、具体的なコマンドの実行例が掲載されています。
Windowsにおいて、VS Code起動中に elan self update
を実行するとエラーになることが報告されています(Issue #95 · leanprover/elan)。
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」チャンネル