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のインストール方法・elanとLakeの使い方

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

Lakeのインストール方法

Lakeに関する用語集

参考資料