プロジェクトの開始
Lean で書かれたプログラムが本格的になるにつれて,Ahead-Of-Time コンパイラベースのワークフローが魅力的になってきます.ほかの言語と同様に,Lean にも複数ファイルのパッケージのビルドと依存関係の管理のためのツールがあります.Lean の標準的なビルドツールは Lake(Lean Make の略)と呼ばれ,Lean で設定されます.Lean には do
記法のように副作用を持つプログラムを書くための特別な言語があるように,Lake にもビルドを設定するための特別な言語があります.これらの言語は埋め込みドメイン固有言語(embedded domain-specific languages)と呼ばれ EDSL と略されます(またはドメイン固有言語(domain-specific languages)とも呼び DSL と略します).EDSL は,あるサブドメインの概念を用いて特定の目的のために使用されるという意味でドメイン固有(domain-specific)であり,一般的に汎用プログラミングには適していません.また,埋め込み(embedded)とはほかの言語の構文の内部で使用されることに由来します.Lean には EDSL を作成するための豊富な機能がありますが,それは本書の範囲外です.
最初のステップ
Lake を使用するプロジェクトを開始するには,greeting
というファイルやディレクトリがまだ存在しないディレクトリで lake new greeting
コマンドを使用します.
Main.lean
は Lean コンパイラがmain
アクションを探すファイルです.Greeting.lean
とGreeting/Basic.lean
はプログラムのサポートライブラリの足場です.lakefile.lean
はlake
がアプリケーションをビルドするために必要な設定を含みます.lean-toolchain
は プロジェクトに使用される Lean の特定のバージョンの識別子を含みます.
さらに,lake new
はプロジェクトを Git リポジトリとして初期化し,.gitignore
ファイルを設定して中間ビルド生成物を無視します.通常,アプリケーションロジックの大部分はプログラム用のライブラリの集まりに含まれ,一方で Main.lean
にはコマンドラインの解析や中心的なアプリケーションロジックの実行を行う小さなラッパーが含まれます.
すでに存在するディレクトリにプロジェクトを作成するには,lake init
の代わりに lake new
を実行します.
デフォルトでは,ライブラリファイル Greeting/Basic.lean
は1つの定義を含みます:
def hello := "world"
ライブラリファイル Greeting.lean
は Greeting/Basic.lean
をインポートします:
-- This module serves as the root of the `Greeting` library.
-- Import modules here that should be built as part of the library.
import «Greeting».Basic
これは,Greetings/Basic.lean
で定義された全てが Greetings.lean
をインポートするファイルでも利用可能であることを意味します.import
文では,ドットはディスク上のディレクトリとして解釈されます.«Greeting»
のように名前の周りに二重山括弧を置くことで,通常 Lean の名前では許されないスペースや他の文字を含むことができます.また,«if»
や «def»
と書くことで,if
や def
のような予約語を通常の名前として使用できます.これにより,lake new
で作成されたパッケージ名にそれらの文字が含まれていた場合の問題を防ぐことができます.
実行可能なソース Main.lean
には以下の内容が含まれています:
import «Greeting»
def main : IO Unit :=
IO.println s!"Hello, {hello}!"
Main.lean
は Greetings.lean
をインポートし,Greetings.lean
は Greetings/Basic.lean
をインポートするので,hello
の定義は main
で使用可能です.
パッケージをビルドするには,lake build
を実行します.いくつかのビルドコマンドがスクロールした後,結果のバイナリは build/bin
に置かれます.
./build/bin/greeting
の実行結果は Hello, world!
です.
Lakefiles
lakefile.lean
は配布用の Lean コードの首尾一貫したコレクションであるパッケージを記述します.これは npm
や nuget
パッケージ,Rust のクレートと似ています.パッケージはいくつかのライブラリや実行可能ファイルを含むことができます.Lake のドキュメント では lakefile で利用可能なオプションについて説明されていますが,ここではまだ説明されていない多くの Lean の機能を利用しています.
生成された lakefile.lean
には以下が含まれています:
import Lake
open Lake DSL
package «greeting» where
-- add package configuration options here
lean_lib «Greeting» where
-- add library configuration options here
@[default_target]
lean_exe «greeting» where
root := `Main
-- Enables the use of the Lean interpreter by the executable (e.g.,
-- `runFrontend`) at the expense of increased binary size on Linux.
-- Remove this line if you do not need such functionality.
supportInterpreter := true
生成直後の Lakefile は3つの項目を含みます:
greeting
という名前のパッケージ宣言Greeting
という名前のライブラリ宣言greeting
という名前の実行ファイル
これらの名前はそれぞれ二重山括弧で囲まれており,ユーザがパッケージ名を自由に選べるようになっています.
各 Lakefile にはちょうど1つのパッケージが含まれますが,ライブラリや実行ファイルはいくつでも含めることができます.さらに,Lakefile は以下も含めることができます:
- 外部ライブラリ(external libraries)- Lean で書かれていませんが,最終的な実行可能ファイルに制的リンクされるライブラリ
- カスタムターゲット(custom targets)- ライブラリ・実行可能ファイルの分類には自然に収まらないビルドターゲット
- 依存関係(dependencies)- 他の Lean パッケージの宣言(ローカルまたは Git リポジトリから取得されます)
- スクリプト(scripts)- 本質的には
main
のようなIO
アクションで,パッケージの設定に関するメタデータにもアクセスできます
Lakefile の項目により,ソースファイルの場所,モジュール階層,コンパイラフラグなどの設定が可能です.しかし一般的にはデフォルト設定が合理的です.
ライブラリ,実行可能ファイル,カスタムターゲットはすべてターゲット(target)と呼ばれます.デフォルトでは,lake build
は @[default_target]
でアノテーションされたターゲットをビルドします.このアノテーションはアトリビュート(attribute)で,Lean の宣言に関連付けることができるメタデータです.アトリビュートは Java のアノテーションや C# や Rust のアトリビュートと似ています.これらは Lean 全体で広く使用されています.
@[default_target]
でアノテーションされていないターゲットをビルドするには,lake build
の後にターゲットの名前を引数として指定します.
ライブラリとインポート
Lean のライブラリは名前をインポートできるソースファイルの階層的に整理されたコレクションで構成され,これをモジュール(moudle)と呼びます.デフォルトでは,ライブラリにはその名前と一致する1つのルートファイルがあります.今回の場合,ライブラリ Greeting
のルートファイルは Greeting.lean
です.
Main.lean
の最初の行 import Greeting
は Greeting.lean
の内容を Main.lean
で使用可能にします.
追加のモジュールファイルをライブラリに追加するには,``Greetingというディレクトリを作成し,その中にファイルを配置します.これらの名前はディレクトリの区切り文字をドットに置き換えることでインポートできます. 例えば,以下の内容の
Greeting/Smile.lean` を作成するとします:
def expression : String := "a big smile"
これにより,Main.lean
は以下のように定義を使用できます:
import Greeting
import Greeting.Smile
def main : IO Unit :=
IO.println s!"Hello, {hello}, with {expression}!"
モジュール名の階層は名前空間の階層と切り離されています.Lean では,モジュールはコード配布の単位で,名前空間はコードの集まりの単位です.つまり,Greeting.Smile
モジュールで定義された名前は,対応する名前空間 Greeting.Smile
に自動的に含まれるわけではありません.モジュールは任意の名前空間に名前を配置でき,インポートするコードはその名前空間を open
するかどうかを選べます.import
はソースファイルの内容を使用可能にするために使用され,open
は名前空間から名前をプレフィックスなしで現在のコンテキストで使用可能にします.Lakefile では,import Lake
の行は Lake
モジュールの内容を使用可能にし,open Lake DSL
の行は Lake
および Lake.DSL
名前空間の内容をプレフィックスなしで使用可能にします.Lake
をオープンすることで Lake.DSL
が DSL
として使用可能となるため,Lake.DSL
もオープンされます.
Lake
モジュールは名前を Lake
と Lake.DSL
名前空間の両方に配置します.
名前空間は選択的にオープンすることもでき,特定の名前だけをプレフィックスなしで使用可能にすることができます.これは,必要な名前を括弧内に書くことで行います.
例えば,Nat.toFloat
は自然数を Float
に変換します.
これを toFloat
として使用可能にするには open Nat (toFloat)
と書きます.