创建项目

随着 Lean 中编写的程序变得越来越复杂，基于提前编译器（Ahead-of-Time，AoT）的工作流变得更具吸引力，因为它可以生成可执行文件。与其他语言类似，Lean 具有构建多文件包和管理依赖项的工具。标准的 Lean 构建工具称为 Lake（「Lean Make」的缩写），它在 Lean 中进行配置。正如 Lean 包含一门用于编写带副作用程序的特殊语言（do 语言）一样， Lake 也包含一门用于配置构建的特殊语言。这些语言被称为 嵌入式领域专用语言（Embedded Domain-Specific Languages） （或有时称为 领域专用嵌入式语言（Domain-Specific Embedded Languages） ，缩写为 EDSL 或 DSEL）。它们是 领域专用（Domain-Specific） 的，因为它们用于专用的目的，包含来自某个子领域的术语，并且通常不适用于通用编程。它们是 嵌入式（Embedded） 的，因为它们出现在另一种语言的语法中。虽然 Lean 包含丰富的用于创建 EDSL 的工具，但它们超出了本书的范围。

入门

要创建一个使用 Lake 的项目，请在一个不包含名为 greeting 的文件或目录的目录下执行命令 lake new greeting，这将创建一个名为 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 包含一个定义：

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!。

Lakefile 构建文件

lakefile.lean 描述了一个 包（Package） ，它是一个连贯的 Lean 代码集合，用于分发，类似于 npm 或 nuget 包或 Rust 的 crate。一个包可以包含任意数量的库或可执行文件。虽然 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 由三项组成：

一个包声明，名为 greeting，
一个库声明，名为 Greeting，以及
一个 可执行文件 ，同样名为 greeting。

这些名称中的每一个都用引号括起来，以允许用户在选择包名称时有更大的自由度。

每个 Lakefile 只会包含一个包，但可以包含任意数量的库或可执行文件。此外，Lakefile 可能包含 外部库（External Library） （即并非用 Lean 编写的库，将与结果可执行文件静态链接）、 自定义目标（Custom Target） （即特定于具体执行平台的库/可执行文件的构建目标）、 依赖项（Dependency） （即其他 Lean 包的声明，可能来自本地或远程 Git 代码库）、以及 脚本（Script） （本质上是类似于 main 的 IO 活动，但还可以访问有关包配置的元数据）。 Lakefile 中的项允许配置源文件位置、模块层次结构和编译器参数。不过一般来说，默认值就够用了。

库、可执行文件和自定义目标统称为 目标（Target） 。默认情况下，lake build 会构建那些标注了 @[default_target] 的目标。此标注是一个 属性（Attribute） ，它是一种可以与 Lean 声明关联的元数据。属性类似于 Java 中的注解或 C# 和 Rust 的特性。它们在 Lean 中被广泛使用。要构建未标注 @[default_target] 的目标，请在 lake build 后指定目标名称作为参数。

库与导入

一个 Lean 库由一个分层组织的源文件集合组成，可以从中导入名称，称为 模块（Module） 。默认情况下，一个库有一个与它名称相同的单一根文件。在本例中，库 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.DSL 已被打开，因为打开 Lake 会让 Lake.DSL 可以只使用名字 DSL 访问，就像 Lake 命名空间中的其他名称一样。Lake 模块将名称放入到了 Lake 和 Lake.DSL 命名空间中。

命名空间也可以 选择性 打开，只公开部分名称而无需显式前缀。这可以通过在括号中写出所需名称来完成。例如，Nat.toFloat 将自然数转换为 Float。可以使用 open Nat (toFloat) 将其公开为 toFloat。

Lean 函数式编程

创建项目

入门

Lakefile 构建文件

库与导入