运行 lake new 将在新目录中创建一个初始的 Lean 包。
此命令等同于创建一个名为 name 的目录，然后运行 lake init。
24.1. Lake
Lake 是标准的 Lean 构建工具。 它负责：
-
配置构建并构建 Lean 代码
-
获取并构建外部依赖
-
与 Reservoir（Lean 包服务器）集成
-
运行测试、代码检查器及其它开发工作流
Lake 是可扩展的。 它提供了一组丰富的接口，可用于为非 Lean 编写的软件工件定义增量构建任务，以自动化管理任务并与外部工作流集成。 对于不需要这些特性的构建配置，Lake 提供了一种声明式配置语言，可以写成 TOML 或 Lean 文件。
本节介绍了 Lake 的 命令行界面、配置文件 以及 内部接口。 这三者共享了一套概念和术语。
24.1.1. 概念与术语
包 是 Lean 代码分发的基本单位。 一个包可以包含多个库或可执行程序。 一个包由一个目录组成，其中包含一个 包配置 文件以及源代码。 包可以 请求 其他包，在这种情况下，这些包的代码（更确切地说，它们的 目标）将变为可用状态。 一个包的 直接依赖 是它所请求的包，而 传递依赖 则是包的直接依赖及其直接依赖的传递依赖。 包可以从 Lean 包仓库 Reservoir 获取，或者从手动指定的位置获取。 Git 依赖 通过 Git 仓库 URL 及修订版本（分支、标签或哈希）指定，并在构建之前必须克隆到本地，而本地的 路径依赖 则通过相对于包目录的路径指定。
工作区 是磁盘上的一个目录，包含一个 包 的源代码工作副本，以及所有未指定为本地路径的 传递依赖 的源代码。
为其创建工作区的包即为 根包。
工作区还包含为该包构建的任何 工件，从而支持 增量构建。
一个目录要被视为工作区，并不需要预先存在依赖和工件；如果它们缺失，诸如 lake update 和 lake build 这样的命令会生成它们。
Lake 通常在工作区中使用。创建工作区的 lake init 和 lake new 是例外。
工作区通常具有以下布局：
-
lean-toolchain：工具链文件。 -
lakefile.toml或lakefile.lean：根包的 包配置 文件。 -
lake-manifest.json：根包的 清单。 -
.lake/：Lake 管理的中间状态，例如已构建的 工件 和依赖源代码。-
.lake/lakefile.olean：根包的配置（已缓存）。 -
.lake/packages/：工作区的 包目录，其中包含根包的所有非本地传递依赖的副本，并在它们各自的.lake目录中包含已构建的工件。 -
.lake/build/：构建目录，其中包含根包的已构建工件：-
.lake/build/bin：包的 二进制目录，其中包含已构建的可执行文件。 -
.lake/build/lib：包的 库目录，其中包含已构建的库和.olean文件。 -
.lake/build/ir：包的中间结果目录，其中包含生成的中间工件，主要是 C 代码。
-
-
包配置 文件指定了一个包的依赖、设置和目标。 包可以指定适用于其包含的所有目标的配置选项。 它们可以用两种格式编写：
清单 追踪包中使用的其他包的特定版本。
清单和 包配置 文件共同为一个包指定了唯一的一组传递依赖。
在构建之前，Lake 会将每个依赖的本地副本与清单中指定的版本同步。
如果没有可用的清单，Lake 会获取每个依赖的最新匹配版本并创建一个清单。
如果清单中列出的包名与包所使用的名称不匹配，则会报错；在构建之前必须使用 lake update 更新清单。
清单应被视为包代码的一部分，通常应检入版本控制系统。
目标 表示用户可以请求的输出。
持久的构建输出，例如目标代码、可执行二进制文件或 .olean 文件，被称为 工件。
在生成工件的过程中，Lake 可能需要生成进一步的工件；例如，将 Lean 程序编译为可执行文件要求它及其依赖被编译为目标文件，而这些文件本身是从 C 源文件生成的，C 源文件则是通过对 Lean 源文件进行精译并生成 .olean 文件 得出的。
该链条中的每个环节都是一个目标，Lake 会安排它们依次构建。
处于链条起点的是 初始目标：
-
包 是作为一个单元分发的 Lean 代码单元。
-
库 是 Lean 模块 的集合，在一个或多个 模块根 下按层次结构组织。
-
可执行文件 由一个定义了
main的单个模块组成。 -
外部库 是非 Lean 的静态库，它们将链接到包及依赖它的包的二进制文件，包括它们的共享库和可执行文件。
-
自定义目标 包含运行构建的任意代码，使用 Lake 的内部接口编写。
除了它们的 Lean 代码外，包、库和可执行文件还包含影响后续构建步骤的配置设置。 包可以指定一组 默认目标。 默认目标是包中要在指定了包但未指定特定目标的上下文中构建的初始目标。
日志 包含在构建期间生成的信息。 保存日志是为了在 增量构建 期间进行重放。 日志中的消息按严重程度分为四个级别：
-
追踪消息包含通常特定于运行构建的机器的内部构建详细信息，包括传递给命令外壳的 Lean 及其他工具的具体调用。
-
信息性消息包含通常不表示代码有问题的常规信息输出，例如
Lean.Parser.Command.eval : command#eval命令的结果。 -
警告指出潜在问题，例如未使用的变量绑定。
-
错误解释为什么解析和精译无法完成。
默认情况下，追踪消息被隐藏，其他的被显示。
阈值可以通过 --log-level 选项、--verbose 标志或 --quiet 标志进行调整。
24.1.1.1. 包覆盖
包配置 和 清单 共同描述了 Lake 获取依赖的精确方式。 通常，这涉及通过网络从远程 Git 仓库获取本地副本。 如果无法访问远程仓库，Lake 会终止并报错。 因为依赖来源是可预测的，所以跨系统的构建是可重现的；在所有机器上都从相同来源以相同方式检索包。
尽管如此，仍存在无法采用与原始开发者相同的方式获取包依赖的情况。 例如，有些公司要求所有依赖在使用前都须经过审计，而且并不是每个人在工作时都能一直连接互联网。 在这些情况下，就有必要通过其他方式获取包。
Lake 的 包覆盖 允许将包依赖从一个源重定向到另一个源，而无需修改任何 包配置 或 清单。
它们不允许在 工作区 中添加或移除包。
工作区中所有的传递依赖都遵守重定向。
包覆盖文件是一个 JSON 文件，包含包条目的备用列表。
这些条目将优先于包的 清单 中的条目。
可以通过 --packages 选项，或者将其放置在 Lake 工作区内的固定路径 .lake/package-overrides.json，来将此文件提供给 Lake。
包覆盖文件中的包条目语法与 清单 的语法一致。
因此，可以把清单中的条目复制到包覆盖文件中（反之亦然）。
确定包条目所需语法的一种方法是：向 包配置 中添加匹配所需配置的临时依赖，运行 lake update 以生成包含该依赖的清单，然后将清单中的条目复制到包覆盖文件中。
本地化远程依赖
考虑这样一个用例：在受限环境（例如出于安全原因）中开发程序，且没有网络连接。
团队希望编译一个用 Lean 编写的依赖于 @leanprover/Cli 库来提供简单命令行界面的小工具。
该工具的 清单 因此如下所示：
{ "version": "1.2.0", "packagesDir": ".lake/packages", "packages": [{ "url": "https://github.com/leanprover/lean4-cli", "type": "git", "subDir": null, "scope": "leanprover", "rev": "0000000000000000000000000000000000000000", "name": "Cli", "manifestFile": "lake-manifest.json", "inputRev": null, "inherited": false, "configFile": "lakefile.toml" }], "name": "myTool", "lakeDir": ".lake", "fixedToolchain": false }
该清单将指示 Lake 在构建此工具时从指定的 GitHub URL 下载 Cli 包。
但是，由于受限环境没有网络连接，如果不使用本地副本，构建将会失败。
这可以通过以下 包覆盖 文件完成：
{ "version": "1.2.0", "packages": [{ "type": "path", "dir": "/etc/lean-packages/Cli", "name": "Cli", "manifestFile": "lake-manifest.json", "inherited": false, "configFile": "lakefile.toml" }] }
有了这个文件，Lake 将把 Cli 依赖解析为位于路径 /etc/lean-packages/Cli 的本地包。
24.1.1.2. 构建
生成所需的 工件，比如 .olean 文件 或可执行二进制文件，被称为 构建。
构建由 lake build 命令或需要工件存在的其他命令（例如 lake exe）触发。
构建包括以下步骤：
- 配置包
如果 包配置 文件比缓存的配置文件
lakefile.olean更新，那么包配置就会被重新精译。 当缓存文件缺失或者提供了--reconfigure或-R标志时，也会发生这种情况。 使用-K对选项的更改不会触发配置文件的重新精译；在这些情况下，必须使用-R。- 计算依赖
确定产生所需输出所需的工件集，以及产生它们的 目标 和 分面。 该过程是递归的，结果是一个依赖图。 图中的依赖与为包声明的依赖不同：包依赖于其他包，而构建目标依赖于其他构建目标，它们可能位于同一个包中，也可能位于不同的包中。 给定目标的一个分面可能依赖于同一目标的其他分面。 Lake 会自动分析 Lean 模块的导入以发现它们的依赖，并且可使用
extraDepTargets字段向目标添加额外的依赖。- 重放追踪
Lake 不会从头开始重建依赖图中的所有内容，而是使用保存的 追踪文件 来确定哪些工件需要构建。 在构建期间，Lake 会记录用于生成每个工件的源文件或其他工件，保存每个输入的哈希；这些 追踪 保存在 构建目录 中。更具体地说，每个工件的追踪文件包含其输入哈希值的 Merkle 树哈希混合。 如果所有输入均未修改，则不再重新构建相应的工件。 追踪文件还额外记录了每个构建任务的 日志；这些输出会被重放，就好像工件被重新构建一样。 在可能的情况下重用先前的构建产物被称为 增量构建。
- 构建工件
当依赖图中所有未修改的依赖都从它们的追踪文件中重放后，Lake 会继续构建每个工件。 这涉及在输入文件上运行适当的构建工具，并按对应分面的指定，保存工件及其追踪文件。
Lake 使用两种不同的哈希算法。 文本文件在规范化换行符之后再进行哈希处理，以便仅因平台特定的换行约定不同而不同的文件也能生成相同的哈希值。 其他文件在哈希时则不作任何规范化。
与追踪文件一样，Lean 会缓存输入哈希。
每当构建一个工件时，其哈希值都会保存在一个独立的文件中，这样可以直接读取该文件，而无需从头计算哈希值。
这是一种性能优化。
可以通过 --rehash 命令行选项禁用此功能，导致所有哈希值都由其输入重新计算。
24.1.1.3. 分面
分面 描述了一个目标从另一个目标的生产过程。
从概念上讲，任何目标都可以拥有分面。
然而，可执行文件、外部库和自定义目标只提供单一的隐式分面。
包、库和模块拥有多个分面，调用 lake build 选定相应目标时，可以通过名称请求它们。
当没有显式请求分面，但指定了初始目标时，lake build 将产生初始目标的 默认分面。
每种类型的初始目标都有相应的默认分面（例如从可执行文件目标生成可执行二进制文件或构建一个包的 默认目标）；可以在 包配置 中或通过 Lake 的 命令行界面 显式请求其他分面。
可以使用 Lake 的内部接口来编写自定义分面。
包可用的分面有：
-
extraDep 包在
extraDepTargets字段中指定的额外依赖目标的默认分面。-
deps 包的 直接依赖。
-
transDeps 包经过拓扑排序的 传递依赖。
-
optCache 包可选的缓存构建归档（例如，来自 Reservoir 或 GitHub）。 如果无法获取归档，不会导致整个构建失败。
-
cache 包的缓存构建归档（例如，来自 Reservoir 或 GitHub）。 如果无法获取归档，将导致整个构建失败。
-
optBarrel 包可选的缓存构建归档（例如，来自 Reservoir 或 GitHub）。 如果无法获取归档，不会导致整个构建失败。
-
barrel 包的缓存构建归档（例如，来自 Reservoir 或 GitHub）。 如果无法获取归档，将导致整个构建失败。
-
optRelease 来自 GitHub 发布版本的包可选构建归档。 如果无法获取发布版本，不会导致整个构建失败。
-
release 来自 GitHub 发布版本的包构建归档。 如果无法获取归档，将导致整个构建失败。
库可用的分面有：
-
leanArts Lean 编译器为库或可执行文件生成的工件（
*.olean、*.ilean和*.c文件）。-
static 由 C 编译器从
leanArts生成的静态库（即*.a文件）。-
static.export 由 C 编译器从
leanArts生成的具有导出符号的静态库（即*.a文件）。-
shared 由 C 编译器从
leanArts生成的共享库（取决于平台，即*.so、*.dll或*.dylib文件）。-
extraDep Lean 库及其所属包的
extraDepTargets。
可执行文件只有一个由可执行二进制文件组成的 exe 分面。
模块可用的分面有：
-
lean 模块的 Lean 源文件。
-
leanArts（默认） 模块的 Lean 工件（
*.olean、*.ilean、*.c文件）。-
deps 模块的依赖（例如导入或共享库）。
-
depHash 模块的构建依赖（例如，导入、源码、插件）的哈希。
-
depTrace 包含模块的构建依赖（例如，导入、源码、插件）的 Lake 构建追踪数据结构（即复合哈希与修改时间）。
-
olean 模块的
.olean文件。-
ilean 模块的
.ilean文件，即 Lean 语言服务器使用的元数据。-
header 模块源文件中解析出的模块头部。
-
input 模块处理过的 Lean 源文件。结合了对文件的追踪与头部的解析。
-
imports Lean 模块的直接导入，但不包含传递导入的全集。
-
precompileImports Lean 模块的传递导入，编译为目标代码。
-
transImports 作为
.olean文件 的 Lean 模块传递导入。-
allImports Lean 模块的直接导入和传递导入。
-
setup 模块的所有依赖：使用
--load-dynlib加载的传递本地导入和共享库。 返回要加载的共享库列表及其搜索路径。-
ir 为使用 模块系统 的模块生成的
.ir文件。-
ir.sig 为使用 模块系统 的模块生成的
.ir.sig文件。-
c 由 Lean 编译器生成的 C 文件。
-
bc 由 Lean 编译器生成的 LLVM 位码文件。
-
c.o 由 C 文件生成的编译目标文件。在 Windows 上它等同于
.c.o.noexport，而在其他平台上它等同于.c.o.export。-
c.o.export 由 C 文件生成的编译目标文件，其中导出了 Lean 符号。
-
c.o.noexport 由 C 文件生成的编译目标文件，其中未导出 Lean 符号。
-
bc.o 由 LLVM 位码文件生成的编译目标文件。
-
o 为配置的后端生成的编译目标文件。
-
dynlib 共享库（例如，用于 Lean 选项
--load-dynlib）。-
ltar 包含模块构建工件的压缩包（通过
leantar生成）。-
linkInfoExport 要链接一个模块及其依赖所需的链接器参数、静态对象和动态库的结构化表示。这些对象会导出 Lean 符号。
-
linkInfoNoExport 要链接一个模块及其依赖所需的链接器参数、静态对象和动态库的结构化表示。这些对象不导出 Lean 符号。
24.1.1.4. 脚本
Lake 包配置 文件可包含 Lake 脚本，这些脚本是可从命令行执行的内嵌程序。
脚本旨在用于特定于项目、且 Lake 的其他特性尚未能很好地处理的任务。
普通的执行程序在 IO 单子 中运行，而脚本在 ScriptM 中运行，后者在 IO 的基础上扩展了有关工作区的信息。
因为它们是 Lean 定义，Lake 脚本只能在 Lean 配置格式中定义。
24.1.1.5. 测试和代码检查驱动程序
测试驱动程序 负责运行一个包的测试。
它可以是可执行目标、Lake 脚本 或库。
Lake 本身并不是测试框架：lake test 命令只是定位已配置的目标，构建它，并且（针对可执行文件和脚本）运行它。
库的驱动程序纯粹通过精译来执行，因此它们不会作为单独的步骤运行。
断言、测试发现以及报告都由目标本身决定，这既可以是第三方测试库，也可以是手写的检查。
对于可执行文件和脚本，Lake 将非零退出代码视为测试失败。
对于库，任何精译错误均算作测试失败，包括 #guard 风格命令的失败。
代码检查驱动程序 也是类似的，只是它由 lake lint 运行，负责检查包在风格及其他方面是否存在不是错误但预示存在潜在问题的状况。
代码检查驱动程序只能是可执行文件或脚本，而不能是库。
24.1.1.5.1. 配置测试驱动程序
在 lakefile.toml 中，将 testDriver 设置为相同配置中定义的可执行文件目标、库目标或脚本的名称：
测试驱动（lakefile.toml）
在 lakefile.lean 中，可以在 package 声明中设置 testDriver 字段（如上所述），也可以使用 test_driver 属性对脚本、可执行文件或库声明进行标记。
属性标记的形式往往更方便，因为它将标记放在了目标旁边。
测试驱动（lakefile.lean）
import Lake
open Lake DSL
package «my-package» where
testDriver := "my-package-tests"
lean_exe «my-package-tests» where
root := `Tests
每个包中只有一个声明可以被标记为 test_driver。
如果在同一 Lake 配置文件中同时使用 test_driver 属性和非空的 testDriver 字段，则会引发错误。
测试驱动程序也可以是传递地 请求 的包依赖项中的目标。
要使用其他包中的目标，请使用 <pkg>/<name> 作为 testDriver 的值，其中 <pkg> 是该目标所在的包的名称。
24.1.1.5.2. 运行测试
lake test 命令仅运行 根包 已配置的驱动程序。
不会运行依赖项的测试驱动程序。
如果测试驱动程序是可执行文件或脚本，Lake 会先传递 testDriverArgs 中的参数，然后传递命令行上 -- 之后的所有内容。
例如，
lake test -- --filter Foo --verbose
将在任何已配置好的 testDriverArgs 后，把 --filter Foo --verbose 传递给驱动程序。
Lake 在运行可执行文件驱动程序前会先对其进行构建。
如果测试驱动程序是库，则不接受参数。
如果 testDriverArgs 不为空，或在 -- 之后有任何参数，Lake 将报告错误。
要运行测试，只需使用 Lean 精译器 对该库进行精译即可。
如果为根包配置了测试驱动程序，lake check-test 将以退出代码 0（即成功）终止。
它不检查所命名的目标是否实际存在。
24.1.1.5.3. 代码检查驱动程序
代码检查驱动程序的配置和运行方式类似于 测试驱动程序。
Lake 配置文件指定一个目标作为代码检查驱动程序，然后由 lake lint 运行它。
此目标必须是可执行文件或脚本；与测试驱动程序不同，代码检查驱动程序不能是库。
在 TOML 格式的 Lake 配置文件中，包级别的 lintDriver 字段指定了代码检查驱动程序目标的名称。
代码检查驱动（lakefile.toml）
在 lakefile.lean 中，可以在 package 声明中设置 lintDriver 字段，也可以使用 lint_driver 属性标记脚本或可执行文件声明。
属性的形式往往更方便，因为它将标记放在了目标旁边。
代码检查驱动（lakefile.lean）
import Lake
open Lake DSL
package «my-package» where
lintDriver := "my-package-lint"
lean_exe «my-package-lint» where
root := `Lint
每个包中只有一个声明可以被标记为 lint_driver。
如果在同一 Lake 配置文件中同时使用 lint_driver 属性和非空的 lintDriver 字段，则会引发错误。
依赖包中的代码检查驱动程序可以使用与测试驱动程序相同的 <pkg>/<name> 语法进行引用。
lake lint 运行已配置的驱动程序，首先传递 lintDriverArgs，然后传递命令行上 -- 之后的任何内容：
lake lint -- --warnings-as-errors
Lake 还有单独的 内置检查器，它直接在 Lean 模块上运行，独立于任何已配置的驱动程序。
内置代码检查可以通过 --builtin-lint 及相关标志（见 lake lint）启用，或通过在包配置中将 builtinLint 设置为 true 来启用。
当内置代码检查启用时，-- 之前的位置参数 MODULE 用于选择要检查的模块，而且它们不会被传递给已配置的驱动程序。
因此 lake lint Mathlib 会触发对 Mathlib 的内置代码检查，而 lake lint -- Mathlib 则会将 Mathlib 传递给驱动程序。
这两种机制相互独立且可同时运行：当它们同时适用时，Lake 将先运行内置检查器，然后再运行驱动程序。
如果为根包配置了代码检查驱动程序，或者其配置中的 builtinLint 被设置为 true，lake check-lint 将以退出代码 0（即成功）退出。
24.1.1.6. GitHub 发布版本构建
Lake 支持将构建工件（即归档后的构建目录）上传到包的 GitHub 发布版本中，或从其中下载。
这使得最终用户能够从云端获取预构建的工件，而无需自己从源码重建整个包。
可以使用 LAKE_NO_CACHE 环境变量来禁用此功能。
24.1.1.6.1. 下载
要下载工件，应配置包选项 releaseRepo 和 buildArchive，使其指向托管发布版本的 GitHub 仓库以及其中正确的工件名称（如果默认设置不充分）。
然后，设置 preferReleaseBuild := true，指示 Lake 将其作为额外的包依赖项获取并解包。
作为标准构建过程的一部分，Lake 仅当需要发布版本构建的包属于依赖时才会获取它（因为根包通常会被修改，所以它往往与此方案不兼容）。
但是，如果希望为根包获取发布版本构建（例如，在克隆发布版本的源代码之后、编辑之前），可以通过 lake build :release 手动执行。
Lake 在内部使用 curl 下载发布版本，并使用 tar 将其解包，因此最终用户必须安装这两种工具才能使用此功能。
如果 Lake 因任何原因未能获取发布版本，它将继续从源代码构建。
该机制在技术上不仅限于 GitHub：任何使用相同 URL 方案的 Git 托管平台同样适用。
24.1.1.6.2. 上传
要将构建的包作为工件上传到 GitHub 发布版本，Lake 提供了 lake upload 命令作为便捷的简写。
此命令使用 tar 将包的构建目录打包为归档，并使用 gh release upload 将其附加到指定标签下预先存在的 GitHub 发布版本中。
因此，为了使用该命令，包的上传者（但不是下载者）需要安装 GitHub 命令行界面 gh 并将其包含在 PATH 中。
24.1.1.7. 工件缓存
这是一项仍在开发中的实验性功能。
Lake 支持 本地工件缓存，该缓存会存储单个构建产物，并追踪生成它们的所有输入集。 每个 工具链 都有其自己的缓存，因为工具链版本之间的中间构建产物是不兼容的。 不过，一个工具链的缓存在使用它的所有本地 工作区 之间是共享的，因此常见的依赖不需要重新构建。 如果两个具有相同工具链的独立工作区依赖于相同的包，则它们可以共享彼此的构建产物。
因为这是一项实验性功能，所以本地缓存默认处于禁用状态。
只有当 LAKE_ARTIFACT_CACHE 环境变量被设置为 true，或者当 enableArtifactCache 字段在 配置文件 中被设置为 true 时才会被启用。
24.1.1.7.1. 远程工件缓存
构建产物可以从远程缓存服务器检索，并放入本地缓存中。
这使得完全避免本地构建成为可能。
lake cache get 命令用于将工件下载到本地缓存中。
与 GitHub 发布版本构建 相比，远程工件缓存的粒度要细得多。
它追踪源代码文件级别、.olean 文件 以及目标代码级别的构建产物，而不是整个包级别的。
24.1.1.7.2. 映射
当传递 -o 选项时，lake build 会追踪用于生成每个构建产物的输入。
它们被存储为 JSON 行格式的 映射文件，文件中每一行都必须是一个有效的 JSON 对象。
一个映射文件追踪单次构建，包括工作区 根包 的所有中间和最终构建产物，但不包含其依赖。
这包括那些已经处于最新状态且不需要重新生成的构建产物。
lake cache put 命令从本地缓存把映射文件中的构建产物上传到远程缓存。
24.1.1.7.3. 配置
使用以下环境变量配置远程工件缓存：
24.1.2. 命令行界面
Lake 的命令行界面结构分为一系列子命令。 所有的子命令都共享由特定的环境变量和全局命令行选项进行配置的能力。 每个子命令都应被理解为一个独立的实用工具，拥有自己必需的实参语法和文档。
一些 Lake 命令委托给了未包含在 Lean 发行版中的其他命令行实用工具。
这些实用工具必须在 PATH 上可用才能使用相应的功能：
-
访问 Git 依赖项需要
git。 -
创建或提取云构建归档文件需要
tar，获取它们需要curl。 -
将构建工件上传到 GitHub 发布版需要
gh。
Lean 发行版包含了 C 编译器工具链。
24.1.2.1. 环境变量
当调用 Lean 编译器或其他工具时，Lake 会设置或修改许多环境变量。
这些值是与系统相关的。
在没有任何实参的情况下调用 lake env 会显示环境变量及其值。
否则，所提供的命令将在 Lake 的环境中被调用。
设置以下变量，覆盖之前的值：
| 检测到的 Lake 可执行文件 |
检测到的 Lake 主目录 | |
检测到的 Lean 工具链目录 | |
检测到的 Lean | |
检测到的 C 编译器（如果不使用绑定的编译器） |
以下变量被增加了附加信息：
| |
| |
| 添加了 Lean 的、Lake 的和 工作区的 二进制目录。 在 Windows 上，也添加了 Lean 的和 工作区的 库目录。 |
| |
|
可以使用以下环境变量配置 Lake 本身：
| |
|
|
|
Lake 安装的位置。
只有当 Lake 无法从当前运行的 |
|
Lean 安装的位置，用于查找 Lean 编译器、标准库和其他绑定工具。
Lake 首先检查其二进制文件是否与 Lean 安装位于同一位置，如果是则使用该安装。
如果不是，或者 |
|
如果设置了 |
|
如果为 true，Lake 不使用来自 Reservoir 或 GitHub 的缓存构建。
可以使用 |
| 如果为 true，Lake 将使用工件缓存。 这是一个实验性功能。 |
| 为远程工件缓存定义认证密钥。 |
|
用于工件上传的远程工件缓存的基准 URL。
如果设置了此变量，则还必须设置 |
|
用于为每个工件上传 输入/输出映射的远程工件缓存的基准 URL。
如果设置了此变量，则还必须设置 |
Lake 将值为 y、yes、t、true、on 或 1（不区分大小写）的环境变量视为 true。
它将值为 n、no、f、false、off 或 0（不区分大小写）的变量视为 false。
如果变量未设置，或者其值既不为 true 也不为 false，则使用默认值。
24.1.2.2. 选项
Lake 的命令行界面提供了许多全局选项以及执行重要任务的子命令。
单字符标志不能组合；-HR 不等于 -H -R。
-
--version Lake 输出其版本并退出，不执行任何其他操作。
-
--help或-h Lake 输出其版本以及使用信息并退出，不执行任何其他操作。 子命令可以与
--help一起使用，在这种情况下将输出该子命令的使用信息。-
--dir=DIR或-d=DIR 将提供的目录而不是当前工作目录用作包的位置。 这并不总是等同于先更改到该目录，因为会使用当前目录的工具链文件指示的
lake版本，而不是DIR的版本。-
--file=FILE或-f=FILE 使用指定的包配置文件而不是默认文件。
-
--old 仅重新构建修改的模块，忽略传递依赖项。 导入修改模块的模块将不会被重新构建。 为了实现这一点，将使用文件修改时间而不是哈希来确定模块是否已更改。
-
--rehash或-H 忽略缓存的文件哈希，重新计算它们。 Lake 使用依赖项的哈希来确定是否重新构建工件。 每当构建模块时，这些哈希都会缓存在磁盘上。 为了在构建过程中节省时间，除非指定了
--rehash，否则会使用这些缓存的哈希，而不是重新计算每个哈希。-
--allow-empty 接受在未配置默认目标时产生无输出的构建。
-
--update 在加载包配置之后、但在执行其他任务（例如构建）之前更新依赖项。 这等同于在选定命令之前运行
lake update，但由于不需要加载配置两次，它可能会更快。-
--packages=FILE 使用指定的包覆盖文件。 可以多次指定此选项以添加更多覆盖（后指定的覆盖优先）。 包覆盖的完整集合还将包括来自
.lake/package-overrides.json的覆盖（如果有）。 但是，通过此选项提供的覆盖具有更高的优先级。-
--reconfigure或-R 通常，包配置文件在首次配置包时由精译器处理，并将结果缓存到供将来调用使用的
.olean文件中，直到包配置发生更改。 提供此标志将导致配置文件被重新精译。-
--keep-toolchain -
--no-build 如果构建目标不是最新的，Lake 会立即退出，并返回非零的退出代码。
-
--no-cache 不使用可用的云构建缓存，而是在本地构建所有包。 构建缓存不被下载。
-
--try-cache 尝试下载支持的包的构建缓存
24.1.2.3. 控制输出
这些选项允许控制在构建时生成的日志。 除了显示或隐藏消息之外，还可以使构建在发出警告甚至信息时失败；这可用于强制实施不允许在构建期间输出的风格指南。
-
--quiet,-q 隐藏信息日志和进度指示器。
-
--verbose,-v 显示跟踪日志（通常是命令调用）和构建的目标。
-
--ansi,--no-ansi 启用或禁用使用为 Lake 的输出添加颜色和动画的 ANSI 转义码。
-
--log-level=LV 设置在构建成功时要显示的日志的最低级别。
LV可以是trace、info、warning或error，不区分大小写。 当构建失败时，会显示所有级别。 默认日志级别为info。-
--fail-level=LV 设置导致构建被视为失败的日志消息级别阈值。 如果在日志中发出的消息级别大于或等于该阈值，构建将失败。
LV可以是trace、info、warning或error，不区分大小写；默认为error。-
--iofail 如果记录了任何 I/O 或其他信息，则导致构建失败。 这等同于
--fail-level=info。-
--wfail 如果记录了任何警告，则导致构建失败。 这等同于
--fail-level=warning。
24.1.2.4. 自动更新工具链
lake update 命令检查依赖项的更改，获取其源代码并相应地更新清单。
默认情况下，当依赖项的新版本指定了更新的工具链时，lake update 还会尝试更新根包的工具链文件。
可以使用 --keep-toolchain 标志禁用此行为。
如果多个依赖项指定了较新的工具链，Lake 将选择最新的兼容工具链（如果存在）。
为了确定最新的兼容工具链，Lake 将包的 lean-toolchain 文件中列出的工具链解析为四类：
-
发布版，按版本号进行比较（例如，
v4.4.0<v4.8.0和v4.6.0-rc1<v4.6.0） -
每日构建版，按日期进行比较（例如，
nightly-2024-01-10<nightly-2024-10-01） -
针对 Lean 编译器的拉取请求构建，不可比较
-
其他版本，同样不可比较
来自多个类别的工具链版本是不可比较的。 如果没有唯一的最新的工具链，Lake 将打印警告并继续更新，而不更改工具链。
如果 Lake 确实找到了新的工具链，那么它会相应地更新工作区的 lean-toolchain 文件，并使用新工具链的 Lake 重新启动 lake update。
如果检测到 Elan，它将通过 elan run 启动新的 Lake 进程，并使用最初运行 Lake 时的相同参数。
如果缺少 Elan，它将提示用户手动重新启动 Lake，并退出特殊的错误代码（即 4）。
可以使用 ELAN 环境变量配置 Lake 使用的 Elan 可执行文件。
24.1.2.5. 创建包
Lake command
lake new name [template][.language]
24.1.2.6. 构建与运行
Lake command
lake build [targets...] [-o mappings]
构建指定的目标的指定分面。
每个 targets 都是通过以下形式的字符串指定的：
[[@]package[/]][target|[+]module][:facet]
可选的 @ 和 + 标记可用于将包和模块与文件路径以及通过按名称作为 target 指定的可执行文件和库区分开来。
如果未提供，package 默认为工作区的根包。
如果工作区中的多个包中存在相同的目标名称，则选择在包依赖关系图的拓扑排序中找到的目标名称的第一次出现。
模块目标也可以由它们的文件名指定，在冒号之后带有可选的分面。
可用的分面取决于要构建的是包、库、可执行文件还是模块。 它们在关于分面的部分中列出。
当使用本地工件缓存时，-o 选项将保存一个跟踪构建每一步的输入和输出的映射文件。
此文件可与 lake cache get 和 lake cache put 一起使用以与远程缓存进行交互。
映射文件采用 JSON Lines 格式，每行一个有效的 JSON 对象，通常文件扩展名为 .jsonl。
目标和分面规范
Lake command
lake check-build
如果工作区的根包配置了任何默认目标，则以状态码 0 退出。 否则报错（退出代码 1）。
lake check-build 不验证配置的默认目标是否有效。
它仅仅验证至少指定了一个。
Lake command
lake query [targets...]
构建一组目标，在标准错误上报告进度，并在标准输出上输出结果。
目标结果按照它们列出的顺序输出，并以换行符结束。
如果设置了 --json，结果将格式化为 JSON。
否则，它们将被打印为原始字符串。
未配置输出的目标将被打印为空字符串或 null。
对于可执行目标，输出是已构建可执行文件的路径。
使用与 lake build 相同的语法指定目标。
Lake command
lake exe exe-target [args...]
Alias: lake exec
在工作区中查找可执行目标 exe-target，如果过期则构建它，然后在 Lake 的环境中使用给定的 args 运行它。
有关目标规范的语法，请参见 lake build，有关如何设置环境的描述，请参见 lake env。
Lake command
lake env [cmd [args...]]
当提供了 cmd 时，它将在带有实参 args 的Lake 环境中执行。
如果没有提供 cmd，Lake 将打印其运行工具的环境。
这个环境是特定于系统的。
24.1.2.7. 模块导入
Lake command
lake shake [options...] [module ...]
通过分析生成的 .olean 文件推断所需的导入，检查当前项目中未使用的导入，确保每个导入都有助于某些常量或其他精译依赖项。
如果指定了 module，则将检查它及其可传递访问的所有文件。否则，将检查包的默认目标。
源文件可以包含特殊的注释来控制 lake shake 的行为：
-
module -- shake: keep-downstream 在所有下游模块中保留此模块。
-
module -- shake: keep-all 保留此模块中的所有现有导入。
-
import X -- shake: keep 保留此特定的导入。
options 可以是：
-
--force 跳过
lake build --no-build健全性检查-
--keep-implied 保留由其他导入隐含的导入
-
--keep-prefix 倾向于父模块导入而不是特定的子模块
-
--keep-public 保留所有的
public导入以保持接口稳定性-
--add-public 如果新导入原本在公开闭包中，则将其添加为
public-
--explain 显示哪些常量需要每次导入
-
--fix 直接将建议的修复应用到源文件
-
--gh-style 以 GitHub 问题匹配器格式输出
24.1.2.8. 开发工具
Lake 包含了对指定标准开发工具和工作流的支持。
在命令行上，可以使用适当的 lake 子命令调用这些工具。
24.1.2.8.1. 测试和代码检查
Lake command
lake test [-- args...]
Lake command
lake lint [options...] [module...] [-- args...]
默认情况下，使用工作区配置的代码检查驱动程序对其根包执行代码检查。
如果在包配置中将 builtinLint 设置为 true，也会运行内置代码检查。
位置实参 module 仅用于缩减内置代码检查 的范围；如果省略，则使用工作区的默认目标根。
调用 代码检查驱动程序时会使用包配置中的 lintDriverArgs 以及位于 -- 之后的任何实参；module 列表不会传递给它。
内置代码检查会在启用了要求的 代码检查器选项的情况下构建目标模块。
它可以通过 --builtin-lint、--builtin-only、--linters、--lint-only，或者在包配置中将 builtinLint 设置为 true 来触发。
相比之下，运行 代码检查驱动程序本身并不会自动触发除了 代码检查驱动程序自身以外的任何构建。
要在某个声明上运行的一组环境代码检查器 由构建该声明时生效的 代码检查器选项决定，不论是通过源文件中的 set_option 还是命令行设置的。
--linters 和 --lint-only 都在执行 代码检查构建时覆盖了这些选项。
options 可以是：
-
--builtin-lint 运行内置的环境和文本代码检查器。
-
--builtin-only 仅运行内置代码检查器，跳过 代码检查驱动程序。
-
--linters<spec> 覆盖 代码检查构建的 代码检查器选项。
<spec>是一个逗号分隔的 代码检查器选项名称列表，每个选项前可以选择带有-以禁用它。 以.开头的名称是linter.前缀的简写，因此.foo表示linter.foo，正如--linters=.foo,-linter.bar那样。 此选项可以重复；对于给定的代码检查器，后面的条目会覆盖前面的。-
--lint-only<spec> 类似于
--linters，但仅报告<spec>明确启用的代码检查器，抑制所有其他代码检查器，包括未命名但默认启用的代码检查器。linter.all和代码检查器集合将被展开。 在--linters和--lint-only之间切换会替换先前的规范。-
--record-exceptions 将每个代码检查器 警告作为
set_option <linter> false in异常记录，通过在原位编辑产生问题的源文件，静默该声明的警告。 这隐含了--builtin-lint。
可以通过设置包配置选项 lintDriver 或使用 @[lint_driver] 属性标记脚本或可执行文件来配置 代码检查驱动程序。
通过将 <pkg>/<name> 语法用于 lintDriver 配置选项，可以将依赖项中的定义用作 代码检查驱动程序。
脚本 代码检查驱动程序将结合包配置的 lintDriverArgs 和 CLI args 运行。
可执行文件 代码检查驱动程序将被构建，然后如同脚本一样运行。
Lake command
lake check-test
检查是否有正确配置的测试驱动程序
如果工作区的根包具有正确配置的测试驱动程序，则以退出码 0 退出。 否则报错（代码 1）。
不验证配置的测试驱动程序是否真正在包或其依赖项中存在。 它仅仅验证是否指定了一个。
这对于区分失败的测试和配置不正确的包很有用。
Lake command
lake check-lint
检查是否有正确配置的代码检查驱动程序
如果工作区的根包具有正确配置的代码检查驱动程序，则以退出码 0 退出。 否则报错（退出代码 1）。
不验证配置的代码检查驱动程序是否真正在包或其依赖项中存在。 它仅仅验证是否指定了一个。
这对于区分失败的代码检查和配置不正确的包很有用。
24.1.2.8.2. 脚本
Lake command
lake script run [[package/]script [args...]]
Lake command
lake script doc script
打印 script 的文档注释。
24.1.2.8.3. 语言服务器
Lake command
lake serve [-- args...]
在工作区的根项目中使用包配置的 moreServerArgs 字段和 args 运行 Lean 语言服务器。
此命令通常由编辑器或其他工具调用，而不是手动调用。
24.1.2.9. 依赖管理
Lake command
lake update [packages...]
更新 Lake 包清单（即，lake-manifest.json），按需下载和升级包。
对于每个新的（传递的）Git 依赖，相应的提交将被克隆到工作区的包目录的一个子目录中。
不对本地依赖项进行复制。
如果指定了一组包 packages，那么这些依赖项将被升级到与包配置兼容的最新版本（或者如果从配置中移除，则被删除）。
如果存在对同一包的多个版本的依赖，则会选择任意一个版本。
单独的 lake update 将升级所有依赖项。
24.1.2.10. 打包和分发
Lake command
lake upload tag
24.1.2.10.1. 缓存的云端构建
这些命令仍然是实验性的。
它们可能会在 Lake 的未来版本中根据用户反馈发生变化。
使用 Reservoir 云构建归档文件的包应启用 platformIndependent 设置。
Lake command
lake pack [archive.tar.gz]
使用 tar 将根包的构建目录打包为 gzip tar 归档文件。
如果未指定归档文件的路径，将在包的 Lake 目录（.lake）中并根据其 buildArchive 设置命名该归档文件。
此命令不构建任何工件：它仅将现有的工件进行归档。
用户在运行此命令之前应确保存在所需的工件。
Lake command
lake unpack [archive.tar.gz]
将 gzip tar 归档文件 archive.tgz 的内容解包到根包的构建目录中。
如果未指定 archive.tgz，将使用包的 buildArchive 设置来决定文件名，并预期该文件在包的 Lake 目录（.lake）中。
24.1.2.11. 本地缓存
lake cache get、lake cache put 和 lake cache add 用于与远程缓存服务器交互。
这些命令是实验性的，并且仅在启用了本地缓存时有用。
可以配置这些命令使用缓存作用域，它是特定于服务器的一个包的一组构建输出的标识符。
在 Reservoir 上，作用域当前与 GitHub 仓库相同，但将来可能包含工具链和平台信息。
其他远程缓存可以使用它们想要的任何作用域方案。
使用 --scope 选项来指定缓存作用域。
缓存作用域不同于用于从 Reservoir 请求包的作用域。
Lake command
lake cache get [mappings] [--max-revs= cn] [--rev= commit-hash] [--package= name] [--service= name] [--repo= github-repo] [--platform= target-triple] [--toolchain=name] [--scope= remote-scope] [--mappings-only] [--force-download]
从远程缓存服务向本地 Lake 工件缓存下载工作区中包的构建输出。
可以通过 --service 选项指定使用的缓存服务。
否则，Lake 将使用系统默认服务；如果未配置任何服务，则使用 Reservoir。
参阅 lake cache services 了解如何配置服务的更多信息。
默认情况下，Lake 将使用 Reservoir 按顺序下载根依赖项树中每个包的输出。
非 Reservoir 依赖将被跳过。
如果提供了输入到输出 mappings 文件、remote-scope 或是 github-repo，Lake 默认将下载根包的构建输出。
无论是哪种情况，--package 都会将下载限制在命名的包的输出上。
对于 Reservoir，设置 --repo 将使 Lake 按仓库名称而不是包名称查找包的输出。
这可以用来下载 Reservoir 包的一个分支的输出（如果此类工件可用的话）。
--platform 和 --toolchain 选项可用于为 Lake 所检测到的平台/工具链之外的配置下载工件。
对于自定义端点，Lake 使用的完整前缀可以通过 --scope 设置。
如果未设置 --rev，Lake 使用包当前的版本来查找工件。
Lake 将为具有可用映射的最新提交下载工件。
它最多将回溯 --max-revs 个版本，默认为 100。
如果设为 0，Lake 将搜索仓库的整个历史记录，或者追溯到 Git 所允许的范围。
默认情况下，Lake 将同时下载包的输入到输出映射和输出工件。
使用 --mappings-only 将使 Lake 仅下载映射，并延迟下载工件，直到它们被需要时为止。
使用 --force-download 将重新下载现有文件。
在下载期间，当某工件的下载失败或整个包的下载过程失败时，Lake 将继续执行。 但是，在这种情况下，它将报告该情况，并以非零状态码退出。
Lake command
lake cache put mappings [--service= name] [--scope= remote-scope] [--repo= github-repo] [--toolchain= name] [--platform= target-triple]
将指定文件中包含的输入到输出映射连同相应的输出工件一起上传到远程缓存。
使用的缓存服务可以通过 --service 选项指定。
如果未指定，Lake 将使用系统默认服务；如果未配置，则会报错。
请参阅 lake cache services 了解有关如何配置服务的更多信息。
文件是通过 curl 使用 AWS Signature Version 4 认证协议上传的。
因此，该服务通常应是一个兼容 S3 的存储桶。
认证密钥通过 LAKE_CACHE_KEY 环境变量设置。
由于 Lake 目前不对工件和输出使用加密安全的哈希，因此缓存的上传以作用域作为前缀以避免冲突。 作用域由以下选项控制：
|
原样使用提供的作用域 |
| 使用仓库、工具链和平台作为作用域 |
|
与 |
|
与 |
对于 --repo，Lake 会通过在认为必要时为仓库添加工具链和平台信息来生成作用域。
对于 --scope，Lake 会原样使用指定的作用域。
工件会以由其 Lake 内容哈希派生的文件名（带有仓库或作用域前缀）上传到工件端点。 映射文件会以由该包当前 Git 版本派生的文件名（带有完整作用域前缀）上传到修订版本端点。 因此，如果工作树目前有更改，命令将会发出警告。
Lake command
lake cache add mappings [--package= name] [--service= name] [--scope= remote-scope] [--repo= github-repo] [--no-overwrite]
从提供的文件中读取一系列输入到输出映射，并将它们添加到本地 Lake 缓存中。
除非指定了 --no-overwrite，否则缓存中已经存在的映射将被覆盖。
除非指定了 --package，否则映射将被添加到根包中。
如果提供了 --service，那么输出工件可以在 Lake 构建期间从该服务延迟获取。
服务必须是 reservoir，或者是通过 Lake 系统配置进行配置的（请参阅 lake cache services 了解详情）。
由于 Lake 目前不对工件和输出使用密码安全哈希，因此缓存服务中的工件会添加作用域前缀，以避免冲突。
对于 Reservoir，该作用域可以是包（通过 --scope 设置）或仓库（通过 --repo 设置）。
对于 S3 服务，这两个选项是同义词。
Lake command
lake cache services
打印每个已配置的远程缓存服务的名称（每行一个）。
可以通过修改系统 Lake 配置文件添加其他服务，该文件通常位于 ~/.lake/config.toml，但也可以通过 LAKE_CONFIG 环境变量进行设置。
系统缓存配置类似如下：
cache.defaultService = "my-s3" cache.defaultUploadService = "my-s3" [[cache.service]] name = "my-s3" kind = "s3" artifactEndpoint = "https://my-s3.com/a0" revisionEndpoint = "https://my-s3.com/r0"
如果没有配置 cache.defaultService，Lake 默认将使用 Reservoir。
Lake command
lake cache stage mappings staging-directory [--force-overwrite]
创建 staging-directory 并将 mappings 文件复制到其中。
在这之后，它会将映射文件中描述的所有工件从缓存复制到暂存目录。
除非指定了 --force-overwrite，否则已经存在于暂存目录中的工件不会被覆盖。
如果无法在缓存中找到描述的任何工件，则报错。
Lake command
lake cache unstage staging-directory [--force-overwrite]
将存储在 staging-directory 中的映射和工件（例如，通过 lake cache stage 生成的）复制回缓存中。
它读取暂存目录内的 outputs.jsonl 处的映射文件，并将该映射写入 Lake 缓存中。然后，它将描述的工件从暂存目录复制到缓存中。
除非指定了 --force-overwrite，否则缓存中已经存在的映射和工件不会被覆盖。
Lake command
lake cache put-staged staging-directory [--rev= commit-hash] [--service= name] [--scope= remote-scope] [--repo= github-repo] [--toolchain= name] [--platform= target-triple]
将存储在 staging-directory 中的映射和工件（例如，通过 lake cache stage 生成的）上传到远程服务。
这与 lake cache put 工作原理类似，区别在于输出取自暂存目录，而不是来自 Lake 工件缓存。
此命令不配置工作区，因此它不执行任意用户代码。
因此，包的平台和工具链设置对于 --repo 是无法自动检测到的，如果需要，必须通过 --platform 和 --toolchain 指定。
默认情况下，Lake 将从工作区目录的当前 Git 版本中检测目标版本。
通过使用 --rev 指定不同的版本，可以上传不同版本的输出。
24.1.2.12. 配置文件
Lake command
lake translate-config lang [out-file]
将已加载的包的配置翻译为 Lake 的另一种受支持的配置语言（即 lean 或 toml）。
生成的文件将写入 out-file，如果未提供，则写入带有新语言扩展名的配置文件路径中。
如果输出文件已存在，Lake 会报错。
翻译是有损的。 它不会保留注释或格式，非声明性配置将被丢弃。
24.1.3. 配置文件格式
Lake 为包配置文件提供两种格式：
- TOML
TOML 配置格式完全是声明式的。 不包含自定义目标、分面或脚本的项目可以使用 TOML 格式。 由于许多语言都有 TOML 解析器，使用这种格式便于和不是用 Lean 编写的工具集成。
- Lean
Lean 配置格式更灵活，允许自定义目标、分面和脚本。 它提供一种嵌入式领域特定语言，用于描述 TOML 格式所提供配置选项的声明式子集。 此外，Lake 接口还可用于表达声明式选项无法表达的构建配置。
lake translate-config 命令可用于在两种格式之间自动转换。
Lake 以类似方式处理这两种格式，并以内部结构类型的形式从配置文件提取包配置。
配置包时，所得数据结构会写入构建目录中的 lakefile.olean。
24.1.3.1. 声明式 TOML 格式
TOMLTom's Obvious Minimal Language 是一种标准化的配置文件格式。 配置文件描述 Lake 包配置文件中最常用的声明式子集。 TOML 文件表示将键映射到值的表。 值可以是字符串、数字、值数组或嵌套的表。 由于 TOML 的文件结构非常灵活，本参考手册记录预期的值，而不是生成这些值的具体语法。
lakefile.toml 的内容应表示描述 Lean 包的 TOML 表。
该配置既包含描述整个包的标量字段，也包含以下由更多表组成的数组字段：
-
require -
lean_lib -
lean_exe
目前，不属于此处所述配置表的字段会被忽略。 为降低拼写错误的风险，这种行为将来可能会改变。 不应使用 Lake 未使用的字段名来存储供其他工具处理的元数据。
24.1.3.1.1. 包配置
lakefile.toml 的顶层内容指定适用于包本身的选项，包括名称和版本等元数据、工作区中文件的位置，以及用于所有目标的编译器标志等。
唯一的必填字段是 name，它声明包的名称。
TOML 表
包配置
Package 的声明式配置。
元数据:
这些选项描述包。 Reservoir 使用它们来索引和显示包。 如果省略某个字段，Reservoir 可能使用包的 GitHub 仓库信息补全细节。
name包含： 包名称
包的名称。
version包含： 版本字符串
包版本。版本形式为：
v!"<major>.<minor>.<patch>[-<specialDescr>]"
带有
-后缀的版本视为“预发行版”。Lake 建议按以下准则递增版本：
-
主版本递增（例如 v1.3.0 → v2.0.0） 表示包中有重大的破坏性变更。 不应期望包使用者无需手动干预就能更新到新版本。
-
次版本递增（例如 v1.3.0 → v1.4.0） 表示通常应向后兼容的重要变更。 应期望包使用者自动更新到此版本，并能轻松修复任何破坏和/或警告。
-
补丁版本递增（例如 v1.3.0 → v1.3.1） 保留用于错误修复和小幅润色。 应期望包使用者自动更新，且除了使用者依赖已修复错误之行为的边缘情况外，不应出现重大破坏。
请注意，任何版本递增都可能发生不向后兼容的变更。 这是因为 Lean 当前的性质（例如传递导入、丰富的元编程、证明中的可约性）使得为包定义完全稳定的 接口并不可行。不同版本级别只表示变更预期的重要程度以及预计迁移的难度。
0.x.x形式的版本视为首次正式发行之前的开发版本。与预发行版一样，它们不必严格遵循上述准则。未定义版本的包默认为
0.0.0。-
versionTags包含： 字符串模式
此包仓库中应视为版本的 Git 标签。 包索引（例如 Reservoir）可利用此信息确定与已发行版本对应的 Git 修订版本。
默认为“类似版本”的标签，即以
v开头、后跟数字的标签。description包含： 字符串
包的简短描述（例如供 Reservoir 使用）。
keywords包含： 由字符串组成的数组
与包关联的自定义关键词。 Reservoir 可使用包的关键词对相关包进行分组，让使用者更容易发现它们。
合适的关键词包括领域（例如
math、software-verification、devtool）、具体子主题（例如topology、cryptology）和重要实现细节（例如dsl、ffi、cli）。例如，Lake 的关键词可以是devtool、cli、dsl、package-manager和build-system。homepage包含： 字符串
指向包相关信息的 URL。
Reservoir 已会包含指向包的 GitHub 仓库的链接（若包来自那里）。因此，建议使用者在此指定其他内容 （如果要指定的话）。
license包含： 字符串
包的许可证（若有）。 应为有效的 SPDX 许可证表达式。
Reservoir 要求包使用 OSI 批准的许可证才能纳入其索引，目前仅支持单标识符 SPDX 表达式。 OSI 批准的 SPDX 许可证标识符列表见 SPDX 许可证列表。
licenseFiles包含： 由路径组成的数组
包含包许可证信息的文件。
这些应是使用者分发包源代码时预期附带的许可证文件；某些许可证可能需要多个文件。例如， Apache 2.0 许可证要求在
NOTICE文件存在时，将它与许可证一起复制。默认为
#["LICENSE"]。readmeFile包含： 路径
包的 README 路径。
README 应为包含包概述的 Markdown 文件。Reservoir 会在包页面上显示该文件渲染后的 HTML。 可以使用非标准位置，分别为 Reservoir 和 GitHub 提供不同的 README。
默认为
README.md。reservoir包含： 布尔值
Reservoir 是否应将包纳入其索引。 设为
false时，Reservoir 不会将包加入索引；若它已在索引中，则会在 Reservoir 下次更新时移除。
布局:
这些选项控制包及其构建目录的顶层目录布局。 包中库、可执行文件和目标指定的其他路径均相对于这些目录。
srcDir包含： 路径
包含包的 Lean 源文件的目录。 默认为包目录。
（它会作为
-R选项传给lean。）buildDir包含： 路径
Lake 应将包的构建结果输出到的目录。 默认为
defaultBuildDir（即.lake/build）。nativeLibDir包含： 路径
Lake 应将包的原生库（例如
.a、.so、.dll文件）输出到的构建子目录。 默认为defaultNativeLibDir（即lib）。binDir包含： 路径
Lake 应将包的二进制可执行文件输出到的构建子目录。 默认为
defaultBinDir（即bin）。irDir包含： 路径
Lake 应将包的中间结果（例如
.c和.o文件）输出到的构建子目录。 默认为defaultIrDir（即ir）。packagesDir包含： 路径
Lake 下载远程依赖项的目录。 默认为
defaultPackagesDir（即.lake/packages）。
构建与运行:
这些选项配置如何在包中构建和运行代码。 包中的库、可执行文件和其他目标可以进一步扩充此配置的某些部分。
extraDepTargets包含： 由字符串组成的数组
每当使用此包时要构建的目标名称
Array。precompileModules包含： 布尔值
是否将包的每个模块编译为原生共享库，并在每次导入该模块时加载。这会加速元程序求值，并让 解释器能够运行标记为
@[extern]的函数。默认为
false。defaultTargets包含： 默认目标名称（数组）
默认构建的包目标名称（即对包执行不带其他参数的
lake build时所构建的目标）。moreGlobalServerArgs包含： 由字符串组成的数组
传给由
lake serve启动的 Lean 语言服务器（即lean --server）的额外实参；既用于此包，也用于 同一会话中从此包浏览的任何包。leanLibDir包含： 路径
Lake 应将包的二进制 Lean 库（例如
.olean、.ilean文件）输出到的构建子目录。 默认为defaultLeanLibDir（即lib/lean）。buildType包含： 以下之一：
"debug","relWithDebInfo","minSizeRel","release"构建模块所采用的模式（例如
debug、release）。 默认为release。leanOptions包含： 由Lean 选项组成的数组
传给由
lake serve启动的 Lean 语言服务器（即lean --server）以及编译模块 Lean 源文件时所用lean的额外选项Array。moreLeanArgs包含： 由字符串组成的数组
编译模块的 Lean 源文件时传给
lean的额外实参。weakLeanArgs包含： 由字符串组成的数组
编译模块的 Lean 源文件时传给
lean的额外实参。与
moreLeanArgs不同，这些实参不影响构建结果的跟踪，因此改变它们不会触发重新构建。 它们位于moreLeanArgs之前。moreLeancArgs包含： 由字符串组成的数组
编译由
lean从模块 C 源文件生成的内容时，传给leanc的额外实参。Lake 已根据
buildType传入一些标志，但可以通过添加-O0和-UNDEBUG等方式改变它们。moreServerOptions包含： 由Lean 选项组成的数组
传给由
lake serve启动的 Lean 语言服务器（即lean --server）的额外选项。weakLeancArgs包含： 由字符串组成的数组
编译由
lean从模块 C 源文件生成的内容时，传给leanc的额外实参。与
moreLeancArgs不同，这些实参不影响构建结果的跟踪，因此改变它们不会触发重新构建。 它们位于moreLeancArgs之前。moreLinkArgs包含： 由字符串组成的数组
链接时传给
leanc的额外实参（例如用于共享库或二进制可执行文件）。 它们位于链接对象路径之后。weakLinkArgs包含： 由字符串组成的数组
链接时传给
leanc的额外实参（例如用于共享库或二进制可执行文件）。 它们位于链接对象路径之后。与
moreLinkArgs不同，这些实参不影响构建结果的跟踪，因此改变它们不会触发重新构建。 它们位于moreLinkArgs之前。platformIndependent包含： 布尔值（可选）
断言 Lake 是否应假定 Lean 模块与平台无关。
-
若为
false，Lake 会将System.Platform.target加入代码单元（例如包或库）内的模块跟踪。 这会强制 Lean 代码在不同平台上重新精译。 -
若为
true，Lake 会从模块跟踪中排除依赖平台的元素（例如预编译模块、外部库），从而避免在 不同平台上重新精译。请注意，这不会影响当前代码单元之外的模块。例如，依赖某个依赖平台库的 平台无关包仍然依赖平台。 -
若为
none，Lake 会自然构造跟踪。也就是说，当模块依赖平台相关产物时就将其纳入跟踪， 否则不会强制模块依赖平台。
此处不会检查正确性，因此配置可以作出不实声明而 Lake 不会发现。默认为
none。-
测试与代码检查:
命令行命令 lake test 和 lake lint 使用由工作区的根包配置的定义来执行测试和代码检查。
为执行测试和代码检查而运行的代码称为测试驱动或代码检查驱动。
在 Lean 配置文件中，可以通过将 @[test_driver] 或 @[lint_driver] 属性应用于Lake 脚本、可执行文件目标或库目标来指定它们。
在 Lean 和 TOML 配置文件中，也可以通过设置这些选项来配置它们。
可以使用字符串 "PKG/TGT" 将依赖项 PKG 中的目标或脚本 TGT 指定为测试或代码检查驱动。
testDriver包含： 字符串
当此包是工作区根时，由
lake test使用的脚本、可执行文件或库的名称。要指向另一包中的定义， 请使用语法<pkg>/<def>。脚本驱动会以
testDriverArgs中配置的实参为先、命令行界面上指定的实参为后（例如通过lake test -- <args>...），由lake test运行。可执行文件驱动会先构建，再像脚本一样运行。 库则只会被构建。testDriverArgs包含： 由字符串组成的数组
传给包的测试驱动的实参。 这些实参位于通过
lake test -- <args>...从命令行传入的实参之前。lintDriver包含： 字符串
当此包是工作区根时，由
lake lint使用的脚本或可执行文件的名称。要指向另一包中的定义， 请使用语法<pkg>/<def>。脚本驱动会以
lintDriverArgs中配置的实参为先、命令行界面上指定的实参为后（例如通过lake lint -- <args>...），由lake lint运行。可执行文件驱动会先构建，再像脚本一样运行。lintDriverArgs包含： 由字符串组成的数组
传给包的代码检查器的实参。 这些实参位于通过
lake lint -- <args>...从命令行传入的实参之前。builtinLint包含： 布尔值（可选）
是否对包运行 Lake 的内置代码检查器。
-
true— 始终运行内置代码检查。若还配置了代码检查驱动，则先运行内置代码检查。 -
false— 默认从不运行内置代码检查。若也未配置代码检查驱动，lake check-lint将以非零代码退出。 -
none（默认值）— 当前等同于false。将来的版本中，未配置代码检查驱动时，none会运行内置 代码检查（即作为回退时等同于true）。
-
云端发行版:
这些选项为包定义云端发行版，详见GitHub 发行版构建一节。
releaseRepo包含： 字符串（可选）
用于上传和下载此包发行版的 GitHub 仓库 URL。 若为
none（默认值），下载时 Lake 使用包的下载来源 URL（若它是依赖项），上传时使用gh的默认值。buildArchive包含： 字符串（可选）
GitHub 云端发行版构建归档的自定义名称。 若为
none（默认值），Lake 使用{(pkg-)name}-{System.Platform.target}.tar.gz。preferReleaseBuild包含： 布尔值
将此包用作依赖项时，是否优先下载（来自 GitHub 的）预构建发行版，而不是从源代码构建此包。
其他字段：
bootstrap包含： 布尔值
供内部使用。 此包是否为 Lean 本身。
enableArtifactCache包含： 布尔值（可选）
是否为包启用 Lake 的本地离线产物缓存。
包的产物（即构建产品）会存入与 Lean 工具链关联的缓存，从而在各本地副本间共享。 使用大型项目或大型依赖项的多个副本时，这可以显著减少初次构建时间和磁盘占用。
需要注意的是，支持产物缓存的构建目标不会存储在构建目录中的通常位置。因此，依赖产物特定位置的 自定义构建脚本可能需要禁用此功能。
若为
none（默认值），则按顺序回退到：-
LAKE_ARTIFACT_CACHE环境变量（若已设置）。 -
工作区根的
enableArtifactCache配置（若已设置且此包是依赖项）。 -
Lake 的默认值：包可以使用缓存中的产物，但不能写入缓存。
-
restoreAllArtifacts包含： 布尔值（可选）
启用本地产物缓存后，Lake 是否应将所有缓存产物复制到构建目录。这可确保外部使用者能在构建目录中 找到构建结果。
若为
none（默认值），则按顺序回退到：-
LAKE_RESTORE_ARTIFACTS环境变量（若已设置）。 -
工作区根的
restoreAllArtifacts配置（若已设置且此包是依赖项）。 -
Lake 的默认值：
false。
-
libPrefixOnWindows包含： 布尔值
此包的原生库在 Windows 上是否应带
lib前缀。与 Unix 不同，Windows 不要求原生库以
lib开头，且按惯例通常也不这样命名。不过，为了在所有 平台上采用一致命名，使用者可能希望启用此选项。默认为
false。allowImportAll包含： 布尔值
下游包是否可以
import all此包的模块。启用后，下游使用者能够访问模块的
private内部实现，包括未标记为@[expose]的定义体。 将来这也可能阻止依赖于private定义无法从其所在包外部访问这一事实的编译器优化。默认为
false。fixedToolchain包含： 布尔值
此包是否预期仅在单一工具链（包的工具链）上工作。
这会告知 Lake 的工具链更新过程（在
lake update中）优先采用此包的工具链，也无需在 Lake 缓存中 按工具链版本区分此包的输入到输出映射。默认为
false。moreLinkObjs包含： 由路径组成的数组
链接（静态和共享）时使用的额外目标对象。 它们位于原生分面路径之后。
moreLinkLibs包含： 由动态库组成的数组
链接时传给
leanc的额外目标库（例如用于共享库或二进制可执行文件）。 它们位于其他链接对象路径之后。requiresModuleSystem包含： 布尔值
此包或库是否应视为面向模块系统设计。
启用后，只要某模块导入此代码单元的模块却没有使用模块系统（即没有
module头部），Lake 就会 发出警告。这既适用于下游使用者，也适用于同一包中的非模块文件，表明该代码单元的接口预期采用 模块系统的可见性与精译语义。导入方可在自己的包或库上设置
allowNonModules := true来选择不接收该警告。默认为
false。allowNonModules包含： 布尔值
此包或库是否允许非模块系统文件而不发出警告。
默认情况下，若此代码单元中的非模块系统文件导入了来自设置了
requiresModuleSystem的代码单元 （可能包括其自身）的模块，Lake 会发出警告。将此项设为true会抑制这些警告，表示该代码单元 明知自己混用了非模块系统文件和模块系统依赖。默认为
false。
24.1.3.1.2. 依赖项
依赖项在包配置的 [[require]] 字段数组中指定，其中同时指定每个包的名称和来源。
来源有三类：
-
Reservoir 或其他包注册表
-
Git 仓库，可以是本地路径或 URL
-
本地路径
TOML 表
引入包 — [[require]]
Dependency 表示包的一个依赖项。
它指定另一个包所依赖的包。
此结构编码 require 领域特定语言语法中包含的信息。
path 和 git 字段为依赖项指定显式来源。
如果两者均未提供，则从 Reservoir 获取依赖项；如果配置了其他注册表，则从该注册表获取。
从 Reservoir 获取包时，必须提供 scope 字段。
字段：
path包含： 路径
本地文件系统中的依赖项，以其路径指定。
git包含： Git 规格
Git 仓库中的依赖项，可以用 URL 字符串指定，也可以用包含以下键的表指定：
-
url：仓库 URL -
subDir：Git 仓库中包含包源代码的子目录
-
rev包含： Git 修订版本
对于 Git 或 Reservoir 依赖项，此字段指定 Git 修订版本，可以是分支名、标签名或特定哈希。 在 Reservoir 上，
version字段优先于此字段。source包含： 包来源
依赖项来源，以独立表指定，在既没有
git键也没有path键时使用。 键type应为字符串"git"或字符串"path"。 如果类型是"path"，则还必须有一个"path"键，其字符串值给出包在磁盘上的位置。 如果类型是"git"，则应提供以下键：-
url：仓库 URL -
rev：Git 修订版本，可以是分支名、标签名或特定哈希（可选） -
subDir：Git 仓库中包含包源代码的子目录
-
version包含： 字符串形式的版本
依赖项的目标版本。
name包含： 字符串
依赖项的包名称。 此名称必须与其配置文件中声明的名称一致，因为该名称用于索引其目标数据类型。为此，包名称还必须 在依赖关系图中的所有包之间唯一。
scope包含： 字符串
用于区分 Lake 注册表中同名包的附加限定符。在 Reservoir 中，这是包所有者。
从 Reservoir 引入包
从 Git 引入包
从 Git 标签引入包
从 Git 标签引入 Reservoir 包
从路径引入包
24.1.3.1.3. 库目标
库目标应写在 lean_lib 表数组中。
TOML 表
库目标 — [[lean_lib]]Lean 库的声明式配置。
字段：
name包含： 库名称
库的名称，通常与其唯一模块根同名。
srcDir包含： 路径
包源目录中包含该库 Lean 源文件的子目录。默认就是上述
srcDir。（它会作为
-R选项传给lean。）roots包含： 由字符串组成的数组
库的根模块。 这些根的子模块（例如
Lib的Lib.Foo）也视为库的一部分。 默认值是仅包含目标名称的单个根。libName包含： 字符串
库产物的名称。 用作其静态和动态二进制文件名的基础。 默认为经过名称改编的目标名称。
libPrefixOnWindows包含： 布尔值
在 Windows 上，此库的静态和共享二进制文件是否应带
lib前缀。与 Unix 不同，Windows 不要求原生库以
lib开头，且按惯例通常也不这样命名。不过，为了在所有 平台上采用一致命名，用户可能希望启用此选项。默认为
false。needs包含： 由目标组成的数组
在库模块之前构建的目标
Array。extraDepTargets包含： 由字符串组成的数组
已弃用。请改用
needs。 在库模块之前构建的目标名称Array。precompileModules包含： 布尔值
是否将库的每个模块编译为原生共享库，并在每次导入该模块时加载。这会加速元程序求值，并让 解释器能够运行标记为
@[extern]的函数。默认为
false。defaultFacets包含： 由字符串组成的数组
对库执行不带其他参数的
lake build时要构建的库分面Array。 例如，#[LeanLib.sharedFacet]会构建共享库分面。allowImportAll包含： 布尔值
下游包是否可以
import all此库的模块。启用后，下游用户能够访问模块的
private内部实现，包括未标记为@[expose]的定义体。 将来这也可能阻止依赖于private定义无法从其所在包外部访问这一事实的编译器优化。默认为
false。buildType包含： 以下之一：
"debug","relWithDebInfo","minSizeRel","release"构建模块所采用的模式（例如
debug、release）。 默认为release。leanOptions包含： 由Lean 选项组成的数组
传给由
lake serve启动的 Lean 语言服务器（即lean --server）以及编译模块 Lean 源文件时所用lean的额外选项Array。moreLeanArgs包含： 由字符串组成的数组
编译模块的 Lean 源文件时传给
lean的额外实参。weakLeanArgs包含： 由字符串组成的数组
编译模块的 Lean 源文件时传给
lean的额外实参。与
moreLeanArgs不同，这些实参不影响构建结果的跟踪，因此改变它们不会触发重新构建。 它们位于moreLeanArgs之前。moreLeancArgs包含： 由字符串组成的数组
编译由
lean从模块 C 源文件生成的内容时，传给leanc的额外实参。Lake 已根据
buildType传入一些标志，但可以通过添加-O0和-UNDEBUG等方式改变它们。moreServerOptions包含： 由Lean 选项组成的数组
传给由
lake serve启动的 Lean 语言服务器（即lean --server）的额外选项。weakLeancArgs包含： 由字符串组成的数组
编译由
lean从模块 C 源文件生成的内容时，传给leanc的额外实参。与
moreLeancArgs不同，这些实参不影响构建结果的跟踪，因此改变它们不会触发重新构建。 它们位于moreLeancArgs之前。moreLinkObjs包含： 由路径组成的数组
链接（静态和共享）时使用的额外目标对象。 它们位于原生分面路径之后。
moreLinkLibs包含： 由动态库组成的数组
链接时传给
leanc的额外目标库（例如用于共享库或二进制可执行文件）。 它们位于其他链接对象路径之后。moreLinkArgs包含： 由字符串组成的数组
链接时传给
leanc的额外实参（例如用于共享库或二进制可执行文件）。 它们位于链接对象路径之后。weakLinkArgs包含： 由字符串组成的数组
链接时传给
leanc的额外实参（例如用于共享库或二进制可执行文件）。 它们位于链接对象路径之后。与
moreLinkArgs不同，这些实参不影响构建结果的跟踪，因此改变它们不会触发重新构建。 它们位于moreLinkArgs之前。platformIndependent包含： 布尔值（可选）
断言 Lake 是否应假定 Lean 模块与平台无关。
-
若为
false，Lake 会将System.Platform.target加入代码单元（例如包或库）内的模块跟踪。 这会强制 Lean 代码在不同平台上重新精译。 -
若为
true，Lake 会从模块跟踪中排除依赖平台的元素（例如预编译模块、外部库），从而避免在 不同平台上重新精译。请注意，这不会影响当前代码单元之外的模块。例如，依赖某个依赖平台库的 平台无关包仍然依赖平台。 -
若为
none，Lake 会自然构造跟踪。也就是说，当模块依赖平台相关产物时就将其纳入跟踪， 否则不会强制模块依赖平台。
此处不会检查正确性，因此配置可以作出不实声明而 Lake 不会发现。默认为
none。-
dynlibs包含： 由动态库组成的数组
在模块精译期间（通过
lean --load-dynlib）加载的动态库目标数组。plugins包含： 由动态库组成的数组
在模块精译期间（通过
lean --plugin）加载的 Lean 插件目标数组。requiresModuleSystem包含： 布尔值
此包或库是否应视为面向模块系统设计。
启用后，只要某模块导入此代码单元的模块却没有使用模块系统（即没有
module头部），Lake 就会 发出警告。这既适用于下游使用者，也适用于同一包中的非模块文件，表明该代码单元的接口预期采用 模块系统的可见性与精译语义。导入方可在自己的包或库上设置
allowNonModules := true来选择不接收该警告。默认为
false。allowNonModules包含： 布尔值
此包或库是否允许非模块系统文件而不发出警告。
默认情况下，若此代码单元中的非模块系统文件导入了来自设置了
requiresModuleSystem的代码单元 （可能包括其自身）的模块，Lake 会发出警告。将此项设为true会抑制这些警告，表示该代码单元 明知自己混用了非模块系统文件和模块系统依赖。默认为
false。
已配置的库目标
此库声明提供更多选项：
[[lean_lib]] name = "TacticTools" srcDir = "src" precompileModules = true
该库的源代码位于 src 目录中，处于以 TacticTools 为根的模块层次结构下。
如果在精译时访问其模块，它们会编译为原生代码并链接进来，而不是在解释器中运行。
24.1.3.1.4. 可执行文件目标
TOML 表
可执行文件目标 — [[lean_exe]]Lean 可执行文件的声明式配置。
字段：
name包含： 可执行文件名称
可执行文件的名称。
srcDir包含： 路径
包源目录中包含该可执行文件 Lean 源文件的子目录。默认就是上述
srcDir。（它会作为
-R选项传给lean。）root包含： 字符串
二进制可执行文件的根模块。 应包含一个作为程序入口点的
main定义。构建该根时会递归构建其本地导入（即工作区中的其他模块）。
默认为目标名称。
exeName包含： 字符串
二进制可执行文件的名称。 默认为将目标名称中的每个
.替换为-后所得的名称。needs包含： 由目标组成的数组
在可执行文件模块之前构建的目标
Array。extraDepTargets包含： 由字符串组成的数组
已弃用。请改用
needs。 在可执行文件模块之前构建的目标名称Array。supportInterpreter包含： 布尔值
通过向 Lean 解释器公开可执行文件中的符号，让该可执行文件能够解释 Lean 文件（例如通过
Lean.Elab.runFrontend）。从实现上说，在 Windows 上会把 Lean 共享库链接到可执行文件；在其他系统上则用
-rdynamic链接可执行文件。这会增大 Linux 上的二进制文件，并且在 Windows 上要求libInit_shared.dll和libleanshared.dll与可执行文件位于同一位置或属于PATH（例如通过lake exe）。因此，只应在 必要时启用此功能。默认为
false。buildType包含： 以下之一：
"debug","relWithDebInfo","minSizeRel","release"构建模块所采用的模式（例如
debug、release）。 默认为release。leanOptions包含： 由Lean 选项组成的数组
传给由
lake serve启动的 Lean 语言服务器（即lean --server）以及编译模块 Lean 源文件时所用lean的额外选项Array。moreLeanArgs包含： 由字符串组成的数组
编译模块的 Lean 源文件时传给
lean的额外实参。weakLeanArgs包含： 由字符串组成的数组
编译模块的 Lean 源文件时传给
lean的额外实参。与
moreLeanArgs不同，这些实参不影响构建结果的跟踪，因此改变它们不会触发重新构建。 它们位于moreLeanArgs之前。moreLeancArgs包含： 由字符串组成的数组
编译由
lean从模块 C 源文件生成的内容时，传给leanc的额外实参。Lake 已根据
buildType传入一些标志，但可以通过添加-O0和-UNDEBUG等方式改变它们。moreServerOptions包含： 由Lean 选项组成的数组
传给由
lake serve启动的 Lean 语言服务器（即lean --server）的额外选项。weakLeancArgs包含： 由字符串组成的数组
编译由
lean从模块 C 源文件生成的内容时，传给leanc的额外实参。与
moreLeancArgs不同，这些实参不影响构建结果的跟踪，因此改变它们不会触发重新构建。 它们位于moreLeancArgs之前。moreLinkObjs包含： 由路径组成的数组
链接（静态和共享）时使用的额外目标对象。 它们位于原生分面路径之后。
moreLinkLibs包含： 由动态库组成的数组
链接时传给
leanc的额外目标库（例如用于共享库或二进制可执行文件）。 它们位于其他链接对象路径之后。moreLinkArgs包含： 由字符串组成的数组
链接时传给
leanc的额外实参（例如用于共享库或二进制可执行文件）。 它们位于链接对象路径之后。weakLinkArgs包含： 由字符串组成的数组
链接时传给
leanc的额外实参（例如用于共享库或二进制可执行文件）。 它们位于链接对象路径之后。与
moreLinkArgs不同，这些实参不影响构建结果的跟踪，因此改变它们不会触发重新构建。 它们位于moreLinkArgs之前。platformIndependent包含： 布尔值（可选）
断言 Lake 是否应假定 Lean 模块与平台无关。
-
若为
false，Lake 会将System.Platform.target加入代码单元（例如包或库）内的模块跟踪。 这会强制 Lean 代码在不同平台上重新精译。 -
若为
true，Lake 会从模块跟踪中排除依赖平台的元素（例如预编译模块、外部库），从而避免在 不同平台上重新精译。请注意，这不会影响当前代码单元之外的模块。例如，依赖某个依赖平台库的 平台无关包仍然依赖平台。 -
若为
none，Lake 会自然构造跟踪。也就是说，当模块依赖平台相关产物时就将其纳入跟踪， 否则不会强制模块依赖平台。
此处不会检查正确性，因此配置可以作出不实声明而 Lake 不会发现。默认为
none。-
dynlibs包含： 由动态库组成的数组
在模块精译期间（通过
lean --load-dynlib）加载的动态库目标数组。plugins包含： 由动态库组成的数组
在模块精译期间（通过
lean --plugin）加载的 Lean 插件目标数组。requiresModuleSystem包含： 布尔值
此包或库是否应视为面向模块系统设计。
启用后，只要某模块导入此代码单元的模块却没有使用模块系统（即没有
module头部），Lake 就会 发出警告。这既适用于下游使用者，也适用于同一包中的非模块文件，表明该代码单元的接口预期采用 模块系统的可见性与精译语义。导入方可在自己的包或库上设置
allowNonModules := true来选择不接收该警告。默认为
false。allowNonModules包含： 布尔值
此包或库是否允许非模块系统文件而不发出警告。
默认情况下，若此代码单元中的非模块系统文件导入了来自设置了
requiresModuleSystem的代码单元 （可能包括其自身）的模块，Lake 会发出警告。将此项设为true会抑制这些警告，表示该代码单元 明知自己混用了非模块系统文件和模块系统依赖。默认为
false。
最小可执行文件目标
24.1.3.2. Lean 格式
Lake 包配置文件的 Lean 格式为 TOML 格式支持的声明式功能提供了一种领域特定语言。
此外，还可以编写 Lean 代码来实现任何无法以声明方式表达的必要构建逻辑。
Lean 配置文件名为 lakefile.lean。
由于 Lean 格式是 Lean 源文件，因此可以使用 Lean 语言服务器的全部功能进行编辑。 此外，Lean 的元编程框架允许使用精译时副作用，实现依赖当前平台的配置步骤等功能。 不过，Lean 配置格式是 Lean 文件，这意味着使用并非以 Lean 编写的工具处理此类文件并不可行。
24.1.3.2.1. 声明式字段
Lean 配置格式的声明式子集使用声明字段序列来指定配置选项。
24.1.3.2.2. 包
语法包配置
command ::= ... |docComment? (@[ attrInstance,* ])? package identOrStr
command ::= ... |docComment? (@[attrInstance,*])? package identOrStr wheredeclField*
command ::= ... |docComment? (@[attrInstance,*])? package identOrStr {declField;* } (whereletRecDecl;*)?
每个 Lake 配置文件只能有一个 Lake.DSL.packageCommand : commandpackage 声明。
已定义的包配置可通过 _package 引用。
语法更新后钩子
command ::= ...
|
为包声明一个执行于 lake update 之后的钩子。
在此包或其下游依赖项之一成功执行 lake update 之后运行该单子动作。
示例
此功能让 Mathlib 能够在 lake update 后同步 Lean 工具链并运行 cache get：
lean_exe cache
post_update pkg do
let wsToolchainFile := (← getRootPackage).dir / "lean-toolchain"
let mathlibToolchain ← IO.FS.readFile <| pkg.dir / "lean-toolchain"
IO.FS.writeFile wsToolchainFile mathlibToolchain
let exeFile ← runBuild cache.fetch
let exitCode ← env exeFile.toString #["get"]
if exitCode ≠ 0 then
error s!"{pkg.name}: failed to fetch cache"
24.1.3.2.3. 依赖项
依赖项使用 Lake.DSL.requireDecl : commandrequire 声明指定。
语法引入包
command ::= ... |docComment require depName (@ git? term)?fromClause? (with term)?
@ 子句指定包版本，用于从 Reservoir 引入包。
版本可以是指定包的 version 字段中所声明版本的字符串，也可以是具体的 Git 修订版本。
Git 修订版本可以是分支名、标签名或提交哈希。
可选的 fromClause
Lake.DSL.requireDecl : commandwith 子句指定用于配置依赖项的 Lake 选项 NameMap String。
这等价于在命令行构建依赖项时向 lake build 传递 -K 选项。
语法包来源
指定获取包依赖项的具体来源。
从远程来源下载的依赖项会放入工作区的 packagesDir。
路径依赖项
from <path>
Lake 会加载相对于依赖方包目录的固定 path 所指位置上的包。
Git 依赖项
from git <url> [@ <rev>] [/ <subDir>]
Lake 会克隆固定 Git url 上可用的 Git 仓库，并检出指定的修订版本 rev。修订版本可以是提交
哈希、分支或标签。若未提供，Lake 默认使用 master。检出后，Lake 会加载位于 subDir 中的包
（若没有指定子目录，则加载仓库根目录中的包）。
fromClause ::=
fromClause ::= ...
| 24.1.3.2.4. 目标
通常通过应用 default_target 属性将目标加入默认目标集合，而不是显式列出它们。
属性指定默认目标
attr ::= ... | default_target
将目标标记为默认目标，在未指定其他目标时构建。
24.1.3.2.4.1. 库
语法库目标
要定义所有可配置字段均使用默认值的库，请使用 Lake.DSL.leanLibCommand : commandlean_lib，不再添加字段。
command ::= ... |docComment? attributes? lean_lib identOrStr
可以通过提供新值来修改默认配置。
command ::= ... |docComment? attributes? lean_lib identOrStr wheredeclField*
command ::= ... |docComment? attributes? lean_lib identOrStr {declField;* } (whereletRecDecl;*)?
Lake.DSL.leanLibCommand : commandlean_lib 的字段就是 LeanLibConfig 结构的字段。
结构体
Lean 库的声明式配置。
扩展
字段
buildType : Lake.BuildType
继承自父结构。
leanOptions : Array Lean.LeanOption
继承自父结构。
moreLeanArgs : Array String
继承自父结构。
weakLeanArgs : Array String
继承自父结构。
moreLeancArgs : Array String
继承自父结构。
moreServerOptions : Array Lean.LeanOption
继承自父结构。
weakLeancArgs : Array String
继承自父结构。
moreLinkObjs : Lake.TargetArray System.FilePath
继承自父结构。
moreLinkLibs : Lake.TargetArray Lake.Dynlib
继承自父结构。
moreLinkArgs : Array String
继承自父结构。
weakLinkArgs : Array String
继承自父结构。
backend : Lake.Backend
继承自父结构。
platformIndependent : Option Bool
继承自父结构。
dynlibs : Lake.TargetArray Lake.Dynlib
继承自父结构。
plugins : Lake.TargetArray Lake.Dynlib
继承自父结构。
requiresModuleSystem : Bool
继承自父结构。
allowNonModules : Bool
继承自父结构。
srcDir : System.FilePath
包源目录中包含该库 Lean 源文件的子目录。默认就是上述 srcDir。
（它会作为 -R 选项传给 lean。）
roots : Array Lean.Name
库的根模块。
这些根的子模块（例如 Lib 的 Lib.Foo）也视为库的一部分。
默认值是仅包含目标名称的单个根。
globs : Array Lake.Glob
要为库构建的模块 Glob 的 Array。
默认为库的每个 roots 各有一个 Glob.one。
子模块通配模式会构建其目录内的每个源文件。 通配模式所匹配文件的本地导入（即工作区中的其他模块）也会递归构建。
libName : String
库产物的名称。 用作其静态和动态二进制文件名的基础。 默认为经过名称改编的目标名称。
libPrefixOnWindows : Bool
在 Windows 上，此库的静态和共享二进制文件是否应带 lib 前缀。
与 Unix 不同，Windows 不要求原生库以 lib 开头，且按惯例通常也不这样命名。不过，为了在所有
平台上采用一致命名，用户可能希望启用此选项。
默认为 false。
needs : Array Lake.PartialBuildKey
在库模块之前构建的目标 Array。
extraDepTargets : Array Lean.Name
已弃用。请改用 needs。
在库模块之前构建的目标名称 Array。
precompileModules : Bool
defaultFacets : Array Lean.Name
对库执行不带其他参数的 lake build 时要构建的库分面 Array。
例如，#[LeanLib.sharedFacet] 会构建共享库分面。
nativeFacets : Bool → Array (Lake.ModuleFacet System.FilePath)
要构建并组合成库的静态库和共享库的模块分面。若 shouldExport 为 true，模块分面应导出用户可能
希望在库中查找的所有符号。例如，Lean 解释器会使用已链接库中的导出符号。
默认为单元素的 Module.oExportFacet（若 shouldExport）或 Module.oFacet。也就是从 Lean 源码
编译得到的目标文件，其中可能带有导出的 Lean 符号。
allowImportAll : Bool
下游包是否可以 import all 此库的模块。
启用后，下游用户能够访问模块的 private 内部实现，包括未标记为 @[expose] 的定义体。
将来这也可能阻止依赖于 private 定义无法从其所在包外部访问这一事实的编译器优化。
默认为 false。
24.1.3.2.4.2. 可执行文件
语法可执行文件目标
要定义所有可配置字段均使用默认值的可执行文件，请使用 Lake.DSL.leanExeCommand : commandlean_exe，不再添加字段。
command ::= ... |docComment? attributes? lean_exe identOrStr
可以通过提供新值来修改默认配置。
command ::= ... |docComment? attributes? lean_exe identOrStr wheredeclField*
command ::= ... |docComment? attributes? lean_exe identOrStr {declField;* } (whereletRecDecl;*)?
Lake.DSL.leanExeCommand : commandlean_exe 的字段就是 LeanExeConfig 结构的字段。
结构体
Lean 可执行文件的声明式配置。
扩展
字段
buildType : Lake.BuildType
继承自父结构。
leanOptions : Array Lean.LeanOption
继承自父结构。
moreLeanArgs : Array String
继承自父结构。
weakLeanArgs : Array String
继承自父结构。
moreLeancArgs : Array String
继承自父结构。
moreServerOptions : Array Lean.LeanOption
继承自父结构。
weakLeancArgs : Array String
继承自父结构。
moreLinkObjs : Lake.TargetArray System.FilePath
继承自父结构。
moreLinkLibs : Lake.TargetArray Lake.Dynlib
继承自父结构。
moreLinkArgs : Array String
继承自父结构。
weakLinkArgs : Array String
继承自父结构。
backend : Lake.Backend
继承自父结构。
platformIndependent : Option Bool
继承自父结构。
dynlibs : Lake.TargetArray Lake.Dynlib
继承自父结构。
plugins : Lake.TargetArray Lake.Dynlib
继承自父结构。
requiresModuleSystem : Bool
继承自父结构。
allowNonModules : Bool
继承自父结构。
srcDir : System.FilePath
包源目录中包含该可执行文件 Lean 源文件的子目录。默认就是上述 srcDir。
（它会作为 -R 选项传给 lean。）
root : Lean.Name
二进制可执行文件的根模块。
应包含一个作为程序入口点的 main 定义。
构建该根时会递归构建其本地导入（即工作区中的其他模块）。
默认为目标名称。
exeName : String
二进制可执行文件的名称。
默认为将目标名称中的每个 . 替换为 - 后所得的名称。
needs : Array Lake.PartialBuildKey
在可执行文件模块之前构建的目标 Array。
extraDepTargets : Array Lean.Name
已弃用。请改用 needs。
在可执行文件模块之前构建的目标名称 Array。
supportInterpreter : Bool
通过向 Lean 解释器公开可执行文件中的符号，让该可执行文件能够解释 Lean 文件（例如通过
Lean.Elab.runFrontend）。
从实现上说，在 Windows 上会把 Lean 共享库链接到可执行文件；在其他系统上则用 -rdynamic
链接可执行文件。这会增大 Linux 上的二进制文件，并且在 Windows 上要求 libInit_shared.dll 和
libleanshared.dll 与可执行文件位于同一位置或属于 PATH（例如通过 lake exe）。因此，只应在
必要时启用此功能。
默认为 false。
nativeFacets : Bool → Array (Lake.ModuleFacet System.FilePath)
要构建并组合成可执行文件的模块分面。
若 shouldExport 为 true，模块分面应导出用户可能希望在可执行文件中查找的所有符号。例如，
Lean 解释器会使用可执行文件中导出的符号。因此，若 supportInterpreter := true，
shouldExport 就会为 true。
默认为单元素的 Module.oExportFacet（若 shouldExport）或 Module.oFacet。也就是从 Lean 源码
编译得到的目标文件，其中可能带有导出的 Lean 符号。
24.1.3.2.4.3. 外部库
由于外部库可以用任意语言编写并需要任意构建步骤，它们被定义为在 FetchM 单子中编写、生成 Job 的程序。
外部库目标应生成一个执行构建并返回所得静态库位置的构建作业。
要使外部库在启用 precompileModules 时正确链接，extern_lib 目标生成的静态库必须遵循平台的库命名约定（即在 Windows 上命名为 foo.a，在类 Unix 系统上命名为 libfoo.a）。
实用函数 Lake.nameToStaticLib 将库名称转换为适合当前平台的文件名。
语法外部库目标
command ::= ... |docComment? attributes? extern_lib identOrStr simpleBinder? := term(where终止提示依次为 `termination_by` 和 `decreasing_by`。letRecDecl*)?
定义新的外部库包目标。只有一种形式：
extern_lib «target-name» (pkg : NPackage _package.name) := /- 构造类型为 `FetchM (Job FilePath)` 的项 -/
pkg 参数（及其类型说明符）可省略。
其类型为 NPackage _package.name，以可证明地表明所提供的包就是定义该目标的包。
该项应构建外部库的静态库。
24.1.3.2.4.4. 自定义目标
可以使用 Lake 接口，以自定义目标定义任意增量构建的产物。
语法自定义目标
command ::= ... |docComment? attributes? target identOrStr simpleBinder? : term := term(where终止提示依次为 `termination_by` 和 `decreasing_by`。letRecDecl*)?
为包定义新的自定义目标。只有一种形式：
target «target-name» (pkg : NPackage _package.name) : α := /- 构造类型为 `FetchM (Job α)` 的项 -/
pkg 参数（及其类型说明符）可省略。
其类型为 NPackage _package.name，以可证明地表明所提供的包就是定义该目标的包。
24.1.3.2.4.5. 自定义分面
自定义分面允许从模块、库或包增量构建额外产物。
语法自定义包分面
包分面允许从整个包生成一个或一组产物。 Lake 接口可查询包中的库；因此，包分面的一个常见用途是构建每个库的指定分面。
command ::= ... |docComment? (@[attrInstance,*])? package_facet identOrStr simpleBinder? : term := term(where终止提示依次为 `termination_by` 和 `decreasing_by`。letRecDecl*)?
定义新的包分面。只有一种形式：
package_facet «facet-name» (pkg : Package) : α := /- 构造类型为 `FetchM (Job α)` 的项 -/
pkg 参数（及其类型说明符）可省略。
语法自定义库分面
库分面允许从库生成一个或一组产物。 Lake 接口可查询库中的模块；因此，库分面的一个常见用途是构建每个模块的指定分面。
command ::= ... |docComment? (@[attrInstance,*])? library_facet identOrStr simpleBinder? : term := term(where终止提示依次为 `termination_by` 和 `decreasing_by`。letRecDecl*)?
定义新的库分面。只有一种形式：
library_facet «facet-name» (lib : LeanLib) : α := /- 构造类型为 `FetchM (Job α)` 的项 -/
lib 参数（及其类型说明符）可省略。
语法自定义模块分面
模块分面允许从模块生成一个或一组产物，通常通过调用命令行工具来完成。
command ::= ... |docComment? (@[attrInstance,*])? module_facet identOrStr simpleBinder? : term := term(where终止提示依次为 `termination_by` 和 `decreasing_by`。letRecDecl*)?
定义新的模块分面。只有一种形式：
module_facet «facet-name» (mod : Module) : α := /- 构造类型为 `FetchM (Job α)` 的项 -/
mod 参数（及其类型说明符）可省略。
24.1.3.2.5. 配置值类型
归纳类型
Lake 中与 CMake 的
CMAKE_BUILD_TYPE 对应的类型。
构造子
Lake.BuildType.debug : Lake.BuildType
调试优化、启用断言、启用自定义调试代码，并在可执行文件中包含调试信息（因此可以在调试器中
单步执行代码，并将地址转换为源文件:行号）。例如，编译 C 代码时传入 -O0 -g。
Lake.BuildType.relWithDebInfo : Lake.BuildType
经过优化，带调试信息，但不含调试代码或断言（例如编译 C 代码时传入
-O3 -g -DNDEBUG）。
Lake.BuildType.minSizeRel : Lake.BuildType
与 release 相同，但优化目标是大小而非速度（例如编译 C 代码时传入 -Os -DNDEBUG）。
Lake.BuildType.release : Lake.BuildType
高优化级别，并且不含调试信息、调试代码或断言（例如编译 C 代码时传入 -O3 -DNDEBUG）。
在 Lake 的 DSL 中，通配模式是匹配模块名称集合的模式。 名称可以强制转换为匹配该名称的通配模式，另有两个后缀运算符用于构造更多通配模式。
语法通配模式语法
通配模式 N.* 匹配 N，或以 N 为前缀的任意子模块。
term ::= ... | name.*
通配模式 N.+ 匹配严格以 N 为前缀的任意子模块，但不匹配 N 本身。
term ::= ... | name.+
名称与 .* 或 .+ 之间不允许有空白。
归纳类型
一组模块名称的规格。
构造子
Lake.Glob.one : Lean.Name → Lake.Glob
仅选择指定的模块名称。
Lake.Glob.submodules : Lean.Name → Lake.Glob
选择指定模块的所有子模块，但不选择模块本身。
Lake.Glob.andSubmodules : Lean.Name → Lake.Glob
选择指定模块及其所有子模块。
结构体
Lean 会像通过 -D 传入一样使用的选项。
字段
name : Lean.Name
选项的名称。
value : Lean.LeanOptionValue
选项的值。
归纳类型
用于编译 Lean 的编译器后端。
构造子
Lake.Backend.c : Lake.Backend
强制使用 C 后端。
Lake.Backend.llvm : Lake.Backend
强制使用 LLVM 后端。
Lake.Backend.default : Lake.Backend
使用默认后端。可由更具体的配置覆盖。
24.1.3.2.6. 脚本
Lake 脚本用于自动化需要访问包配置、但不参与从代码增量构建产物的任务。
脚本在 ScriptM 单子中运行；它是在 IO 上叠加一个提供包配置访问能力的读取器单子变换器。
具体而言，脚本应具有类型 List String → ScriptM UInt32。
脚本主要通过 MonadWorkspace ScriptM 实例访问工作区信息。
语法脚本声明
command ::= ... |docComment? (@[attrInstance,*])? script identOrStr simpleBinder? := term(where终止提示依次为 `termination_by` 和 `decreasing_by`。letRecDecl*)?
定义新的 Lake 脚本。
示例
/-- 显示问候语 -/
script «script-name» (args) do
if h : 0 < args.length then
IO.println s!"Hello, {args[0]'h}!"
else
IO.println "Hello, world!"
return 0
定义
Lake.ScriptM (α : Type) : TypeLake.ScriptM (α : Type) : Type
Script 所用的单子类型。
它是一个 IO 单子，并配备了有关 Lake 配置的信息。
24.1.3.2.7. 实用工具
语法当前目录
term ::= ...
| 在 Lakefile 精译期间展开为包目录路径的宏。
语法配置选项
term ::= ...
|
在 Lakefile 精译期间展开为指定配置选项的宏；若尚未设置该选项，则展开为 none。
配置实参可以通过 Lake 命令行界面（使用 -K 选项）设置，也可以通过 require 语句中的 with
子句设置。
语法编译时条件
command ::= ... |meta if term thencmdDo (elsecmdDo)?
meta if 命令有两种形式：
meta if <c:term> then <a:command> meta if <c:term> then <a:command> else <b:command>
若项 c（在精译时）求值得到 true，它会展开为命令 a。否则，它会展开为命令 b（若提供了
else 子句）。
例如，可以使用此命令来指定仅在特定平台上可用的外部库目标：
meta if System.Platform.isWindows then extern_lib winOnlyLib := ... else meta if System.Platform.isOSX then extern_lib macOnlyLib := ... else meta if System.Platform.isLinux then extern_lib linuxOnlyLib := ...
语法命令序列
cmdDo ::= ...
| cmdDo ::= ...
|
do 命令语法把多个缩进相同的命令组合在一起。
随后可将这组命令传给通常只接受单个命令的另一条命令（例如 meta if）。
24.1.4. 脚本接口参考
除了普通的 IO 效应，Lake 脚本还能访问 Lake 环境（它提供了有关当前工具链的信息，例如 Lean 编译器的位置）以及当前的工作区。
这一访问权限是在 ScriptM 中提供的。
定义
Lake.ScriptM (α : Type) : TypeLake.ScriptM (α : Type) : Type
Script 所用的单子类型。
它是一个 IO 单子，并配备了有关 Lake 配置的信息。
24.1.4.1. 访问环境
提供对当前 Lake 环境信息（例如 Lean、Lake 以及其它工具的位置）访问权限的单子具备 MonadLakeEnv 实例。
Lake 接口中的所有单子皆是如此，包括 ScriptM。
定义
配备了（只读的）已探测 Lake 环境的单子。
定义
获取当前 Lake 环境。
定义
Lake.getNoCache.{u_1} {m : Type → Type u_1} [Lake.MonadLakeEnv m] [Functor m] [Lake.MonadBuild m] : m BoolLake.getNoCache.{u_1} {m : Type → Type u_1} [Lake.MonadLakeEnv m] [Functor m] [Lake.MonadBuild m] : m Bool
返回 Lake 配置中的 LAKE_NO_CACHE/。
定义
Lake.getTryCache.{u_1} {m : Type → Type u_1} [Lake.MonadLakeEnv m] [Functor m] [Lake.MonadBuild m] : m BoolLake.getTryCache.{u_1} {m : Type → Type u_1} [Lake.MonadLakeEnv m] [Functor m] [Lake.MonadBuild m] : m Bool
返回 Lake 配置中的 LAKE_NO_CACHE/ 是否未设置。
定义
Lake.getPkgUrlMap.{u_1} {m : Type → Type u_1} [Lake.MonadLakeEnv m] [Functor m] : m (Lean.NameMap String)Lake.getPkgUrlMap.{u_1} {m : Type → Type u_1} [Lake.MonadLakeEnv m] [Functor m] : m (Lean.NameMap String)
返回 Lake 环境的 LAKE_PACKAGE_URL_MAP。若不存在则为空。
定义
返回 Lake 环境的 Elan 工具链名称。若不存在则为空。
24.1.4.1.1. 搜索路径辅助函数
定义
Lake.getEnvLeanPath.{u_1} {m : Type → Type u_1} [Lake.MonadLakeEnv m] [Functor m] : m System.SearchPathLake.getEnvLeanPath.{u_1} {m : Type → Type u_1} [Lake.MonadLakeEnv m] [Functor m] : m System.SearchPath
返回 Lake 环境中探测到的 LEAN_PATH 值。
定义
Lake.getEnvLeanSrcPath.{u_1} {m : Type → Type u_1} [Lake.MonadLakeEnv m] [Functor m] : m System.SearchPathLake.getEnvLeanSrcPath.{u_1} {m : Type → Type u_1} [Lake.MonadLakeEnv m] [Functor m] : m System.SearchPath
返回 Lake 环境中探测到的 LEAN_SRC_PATH 值。
24.1.4.1.2. Elan 安装辅助函数
定义
Lake.getElanInstall?.{u_1} {m : Type → Type u_1} [Lake.MonadLakeEnv m] [Functor m] : m (Option Lake.ElanInstall)Lake.getElanInstall?.{u_1} {m : Type → Type u_1} [Lake.MonadLakeEnv m] [Functor m] : m (Option Lake.ElanInstall)
返回探测到的 Elan 安装（若存在）。
定义
Lake.getElanHome?.{u_1} {m : Type → Type u_1} [Lake.MonadLakeEnv m] [Functor m] : m (Option System.FilePath)Lake.getElanHome?.{u_1} {m : Type → Type u_1} [Lake.MonadLakeEnv m] [Functor m] : m (Option System.FilePath)
返回探测到的 Elan 安装的根目录（即 ELAN_HOME）。
定义
Lake.getElan?.{u_1} {m : Type → Type u_1} [Lake.MonadLakeEnv m] [Functor m] : m (Option System.FilePath)Lake.getElan?.{u_1} {m : Type → Type u_1} [Lake.MonadLakeEnv m] [Functor m] : m (Option System.FilePath)
返回探测到的 Elan 安装中 elan 二进制文件的路径。
24.1.4.1.3. Lean 安装辅助函数
定义
Lake.getLeanInstall.{u_1} {m : Type → Type u_1} [Lake.MonadLakeEnv m] [Functor m] : m Lake.LeanInstallLake.getLeanInstall.{u_1} {m : Type → Type u_1} [Lake.MonadLakeEnv m] [Functor m] : m Lake.LeanInstall
返回探测到的 Lean 安装。
定义
Lake.getLeanSysroot.{u_1} {m : Type → Type u_1} [Lake.MonadLakeEnv m] [Functor m] : m System.FilePathLake.getLeanSysroot.{u_1} {m : Type → Type u_1} [Lake.MonadLakeEnv m] [Functor m] : m System.FilePath
返回探测到的 Lean 安装的根目录。
定义
Lake.getLeanSrcDir.{u_1} {m : Type → Type u_1} [Lake.MonadLakeEnv m] [Functor m] : m System.FilePathLake.getLeanSrcDir.{u_1} {m : Type → Type u_1} [Lake.MonadLakeEnv m] [Functor m] : m System.FilePath
返回探测到的 Lean 安装的 Lean 源码目录。
定义
Lake.getLeanLibDir.{u_1} {m : Type → Type u_1} [Lake.MonadLakeEnv m] [Functor m] : m System.FilePathLake.getLeanLibDir.{u_1} {m : Type → Type u_1} [Lake.MonadLakeEnv m] [Functor m] : m System.FilePath
返回探测到的 Lean 安装的 Lean 库目录。
定义
Lake.getLeanIncludeDir.{u_1} {m : Type → Type u_1} [Lake.MonadLakeEnv m] [Functor m] : m System.FilePathLake.getLeanIncludeDir.{u_1} {m : Type → Type u_1} [Lake.MonadLakeEnv m] [Functor m] : m System.FilePath
返回探测到的 Lean 安装的 C 头文件目录。
定义
Lake.getLeanSystemLibDir.{u_1} {m : Type → Type u_1} [Lake.MonadLakeEnv m] [Functor m] : m System.FilePathLake.getLeanSystemLibDir.{u_1} {m : Type → Type u_1} [Lake.MonadLakeEnv m] [Functor m] : m System.FilePath
返回探测到的 Lean 安装的系统库目录。
定义
返回探测到的 Lean 安装中 lean 二进制文件的路径。
定义
返回探测到的 Lean 安装中 leanc 二进制文件的路径。
定义
返回探测到的 Lean 安装中 ar 二进制文件的路径。
定义
返回探测到的 Lean 安装中 C 编译器的路径。
定义
返回探测到的 Lean 安装中可选的 LEAN_CC 编译器覆盖值。
24.1.4.1.4. Lake 安装辅助函数
定义
Lake.getLakeInstall.{u_1} {m : Type → Type u_1} [Lake.MonadLakeEnv m] [Functor m] : m Lake.LakeInstallLake.getLakeInstall.{u_1} {m : Type → Type u_1} [Lake.MonadLakeEnv m] [Functor m] : m Lake.LakeInstall
返回探测到的 Lake 安装。
定义
返回探测到的 Lake 安装的根目录（例如 LAKE_HOME）。
定义
Lake.getLakeSrcDir.{u_1} {m : Type → Type u_1} [Lake.MonadLakeEnv m] [Functor m] : m System.FilePathLake.getLakeSrcDir.{u_1} {m : Type → Type u_1} [Lake.MonadLakeEnv m] [Functor m] : m System.FilePath
返回探测到的 Lake 安装的源码目录。
定义
Lake.getLakeLibDir.{u_1} {m : Type → Type u_1} [Lake.MonadLakeEnv m] [Functor m] : m System.FilePathLake.getLakeLibDir.{u_1} {m : Type → Type u_1} [Lake.MonadLakeEnv m] [Functor m] : m System.FilePath
返回探测到的 Lake 安装的 Lean 库目录。
定义
返回探测到的 Lake 安装中 lake 二进制文件的路径。
24.1.4.2. 访问工作区
提供对当前 Lake 工作区信息访问权限的单子具备 MonadWorkspace 实例。
特别是，有针对 ScriptM 和 LakeM 的实例。
类型类
配备了（只读的）Lake Workspace 的单子。
实例构造子
Lake.MonadWorkspace.mk.{u}
方法
getWorkspace : m Lake.Workspace
获取当前 Lake 工作区。
定义
Lake.getRootPackage.{u_1} {m : Type → Type u_1} [Lake.MonadWorkspace m] [Functor m] : m Lake.PackageLake.getRootPackage.{u_1} {m : Type → Type u_1} [Lake.MonadWorkspace m] [Functor m] : m Lake.Package
返回上下文工作区的根包。
定义
Lake.findPackageByName?.{u_1} {m : Type → Type u_1} [Lake.MonadWorkspace m] [Functor m] (name : Lean.Name) : m (Option Lake.Package)Lake.findPackageByName?.{u_1} {m : Type → Type u_1} [Lake.MonadWorkspace m] [Functor m] (name : Lean.Name) : m (Option Lake.Package)
返回工作区中首个（若存在）被赋予 name 的包。
这可用于查找与用户提供的名称对应的包。如果已经有该包的唯一标识符，请改用
findPackageByKey?。
定义
Lake.findPackageByKey?.{u_1} {m : Type → Type u_1} [Lake.MonadWorkspace m] [Functor m] (keyName : Lean.Name) : m (Option (Lake.NPackage keyName))Lake.findPackageByKey?.{u_1} {m : Type → Type u_1} [Lake.MonadWorkspace m] [Functor m] (keyName : Lean.Name) : m (Option (Lake.NPackage keyName))
返回工作区中由 keyName 标识的唯一包（若存在）。
定义
Lake.findModule?.{u_1} {m : Type → Type u_1} [Lake.MonadWorkspace m] [Functor m] (name : Lean.Name) : m (Option Lake.Module)Lake.findModule?.{u_1} {m : Type → Type u_1} [Lake.MonadWorkspace m] [Functor m] (name : Lean.Name) : m (Option Lake.Module)
在工作区中定位具有给定名称、可构建、可导入且位于本地的模块。
定义
Lake.findLeanExe?.{u_1} {m : Type → Type u_1} [Lake.MonadWorkspace m] [Functor m] (name : Lean.Name) : m (Option Lake.LeanExe)Lake.findLeanExe?.{u_1} {m : Type → Type u_1} [Lake.MonadWorkspace m] [Functor m] (name : Lean.Name) : m (Option Lake.LeanExe)
尝试在工作区中查找具有给定名称的 Lean 可执行文件。
定义
Lake.findLeanLib?.{u_1} {m : Type → Type u_1} [Lake.MonadWorkspace m] [Functor m] (name : Lean.Name) : m (Option Lake.LeanLib)Lake.findLeanLib?.{u_1} {m : Type → Type u_1} [Lake.MonadWorkspace m] [Functor m] (name : Lean.Name) : m (Option Lake.LeanLib)
尝试在工作区中查找具有给定名称的 Lean 库。
定义
Lake.findExternLib?.{u_1} {m : Type → Type u_1} [Lake.MonadWorkspace m] [Functor m] (name : Lean.Name) : m (Option Lake.ExternLib)Lake.findExternLib?.{u_1} {m : Type → Type u_1} [Lake.MonadWorkspace m] [Functor m] (name : Lean.Name) : m (Option Lake.ExternLib)
尝试在工作区中查找具有给定名称的外部库。
定义
Lake.getLeanPath.{u_1} {m : Type → Type u_1} [Lake.MonadWorkspace m] [Functor m] : m System.SearchPathLake.getLeanPath.{u_1} {m : Type → Type u_1} [Lake.MonadWorkspace m] [Functor m] : m System.SearchPath
返回上下文工作区添加到 LEAN_PATH 的路径。
定义
Lake.getLeanSrcPath.{u_1} {m : Type → Type u_1} [Lake.MonadWorkspace m] [Functor m] : m System.SearchPathLake.getLeanSrcPath.{u_1} {m : Type → Type u_1} [Lake.MonadWorkspace m] [Functor m] : m System.SearchPath
返回上下文工作区添加到 LEAN_SRC_PATH 的路径。
定义
Lake.getAugmentedLeanPath.{u_1} {m : Type → Type u_1} [Lake.MonadWorkspace m] [Functor m] : m System.SearchPathLake.getAugmentedLeanPath.{u_1} {m : Type → Type u_1} [Lake.MonadWorkspace m] [Functor m] : m System.SearchPath
返回上下文工作区设置的扩充后 LEAN_PATH。
定义
Lake.getAugmentedLeanSrcPath.{u_1} {m : Type → Type u_1} [Lake.MonadWorkspace m] [Functor m] : m System.SearchPathLake.getAugmentedLeanSrcPath.{u_1} {m : Type → Type u_1} [Lake.MonadWorkspace m] [Functor m] : m System.SearchPath
返回上下文工作区设置的扩充后 LEAN_SRC_PATH。
定义
Lake.getAugmentedEnv.{u_1} {m : Type → Type u_1} [Lake.MonadWorkspace m] [Functor m] : m (Array (String × Option String))Lake.getAugmentedEnv.{u_1} {m : Type → Type u_1} [Lake.MonadWorkspace m] [Functor m] : m (Array (String × Option String))
返回上下文工作区设置的扩充后环境变量。