プロジェクトの開始

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) と書きます．

Functional Programming in Lean 日本語訳

プロジェクトの開始

最初のステップ

Lakefiles

ライブラリとインポート