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 に詳細な情報が書かれています。