Lake 官方文档¶

Lake（Lean Make）是 Lean 4 新的构建系统和包管理器。借助 Lake，包的配置可以写入位于包根目录下的专用 lakefile.lean 文件中。

每个 lakefile.lean 文件包含一个 package 声明（类似于 main 函数），用于定义包的基本配置。通常，还包括不同目标的构建配置（例如 Lean 库文件和二进制可执行文件），以及通过 lake script run 运行的命令行脚本。

此 README 提供了与当前提交相关的 Lake 信息。如果您正在查找随特定 Lean 版本发布的 Lake 文档，请查看该版本的 README。

获取 Lake¶

Lake 是 lean4 仓库的一部分，随其官方版本一同发布（例如，作为 elan 工具链的一部分）。所以，如果你已经安装了近期版本的 Lean 4，你也应该已经拥有了 Lake！如果你想自己从源码构建最新版本，请参阅此 README 最后的构建指南。

创建并构建一个包¶

要创建一个新包，可以运行 lake init 在当前目录中设置包，或运行 lake new 在新目录中创建包。例如，我们可以这样创建包 hello：

$ mkdir hello
$ cd hello
$ lake init hello

或者这样：

$ lake new hello
$ cd hello

无论采用哪种方式，Lake 都会创建如下模板目录结构并为包初始化一个 Git 仓库。

.lake/         # Lake 的输出目录
Hello/         # 库的源文件目录; 通过 `import Hello.*` 导入
  Basic.lean   # 一个示例库模块文件
  ...          # 在此处添加其他文件
Hello.lean     # 库的根文件; 从 Hello 导入标准模块
Main.lean      # 可执行文件的主文件 (含 `def main`)
lakefile.lean  # Lake 的包配置文件
lean-toolchain # 包所使用的 Lean 版本
.gitignore     # 排除系统特定文件 (如 `build`) 从 Git 版本控制中

示例模块文件包含以下 "Hello World" 程序。

Hello/Basic.lean

def hello := "world"

Hello.lean

-- 这个模块是 `Hello` 库的根文件
-- 在这里导入应作为库一部分构建的模块。
import «Hello».Basic

Main.lean

import «Hello»

def main : IO Unit :=
  IO.println s!"Hello, {hello}!"

Lake 还会为包创建一个基础的 lakefile.lean 文件以及一个包含 Lean 工具链名称的 lean-toolchain 文件，这样 elan 就知道该为这个包使用哪个 Lean 工具链。

lakefile.lean

import Lake
open Lake DSL

package «hello» where
  -- 在此添加包配置选项

lean_lib «Hello» where
  -- 在此添加库配置选项

@[default_target]
lean_exe «hello» where
  root := `Main

lake build 命令用于构建包（及其依赖项，如果有的话）为本地可执行文件。结果将放置在 .lake/build/bin 目录下。lake clean 命令会删除 build 目录。

$ lake build
...
$ ./.lake/build/bin/hello
Hello, world!

在此仓库的 examples 文件夹中可以找到不同包配置的示例。你也可以为 lake init 或 lake new 命令传入模板以控制 Lake 创建的文件。例如，你可以通过 lake new hello .toml 命令生成一个 TOML 版本的配置文件，而不是使用 Lean 配置文件。

lakefile.toml

name = "hello"
defaultTargets = ["hello"]

[[lean_lib]]
name = "Hello"

[[lean_exe]]
name = "hello"
root = "Main"

使用 lake help init 或 lake help new 命令可以查看有关其他模板选项的更多详细信息。

术语表¶

在软件开发过程中，Lake 会用到一系列的术语 —— 如工作空间（workspace）、包（package）、库（library）、可执行文件（executable）、目标（target）等等 —— 还有些更难理解的术语，如 facet。不过，无论这些术语是否常见，不同的人对其都有着不同的理解，因此有必要明确 Lake 对这些术语的定义：

包（package） 是 Lake 代码分发的基本单元。包可以来源于本地文件系统，也可以从网络下载（如通过 Git）。包的 lakefile 中的 package 声明决定了包的名称，并定义其基本属性。

lakefile 是记录整个包配置的 Lean 文件。它定义了如何查看、编辑、构建和运行包中的代码，并指定了所依赖的其它包。

如果包 B 依赖包 A，包 A 就是包 B 的依赖（dependency），而包 B 就是包 A 的 下游依赖（dependent）。包 A 是包 B 的上游，反之包 B 是包 A 的下游。参见添加依赖以了解如何指定依赖。

工作空间（workspace） 是 Lake 中 最大的组织单元。它将一个被称为 root(根) 的包、传递的依赖以及 Lake 的环境组合在一起。每个包都可以作为工作区的根，并且工作区将从这个根派生其配置。

模块（module） 是 Lake 构建系统可见的最小代码单元。模块通常由一个 Lean 源文件和一组二进制库文件（如 olean 和 ilean，若开启 precompileModules 选项，还包括系统共享库）组成。模块之间可以相互导入以使用彼此的代码，Lake 的主要作用就是促进这一过程。

Lean 库（Lean library） 是一组共享同一配置的模块集合。其配置定义了一组 模块根（module roots），用于确定哪些模块属于该库，以及一组 模块全局模式（module globs），用于在库的 lake build 过程中选择要构建的模块。参见Lean 库部分了解更多详情。

Lean 二进制可执行文件（Lean binary executable） 是一个由根模块（其中应包含 main 定义）构建的二进制可执行文件（即用户在未安装 Lean 时就能在电脑上运行的程序）。参见二进制可执行文件部分了解更多详情。

外部库（external library） 是由外部代码（如 C 语言）构建的原生（静态）库，Lean 代码需要这些库来实现功能（例如，使用 @[extern] 调用外部代码）。extern_lib 目标用于告知 Lake 此类需求并指示 Lake 如何构建必要的库。Lake 随后会在适当时自动链接外部库，以便使 Lean 代码能够访问所需的外部函数（或更专业地说，是外部符号）。参见外部库部分了解更多详情。

目标（target） 是 Lake 构建的基本单元。一个包可以定义任意数量的目标。每个目标都有一个名称，用于指示 Lake 去构建该目标（例如，通过 lake build <target>）并在内部跟踪目标的构建状态。Lake 定义了一组内置目标类型 —— Lean 库、二进制可执行文件和外部库 —— 但用户也可以定义自己的自定义目标。复杂类型（如包、库、模块）具有多个 facet，每个 facet 都算作独立的可构建目标。参见定义构建目标部分了解更多详情。

facet 是从其它组织单位构建出的单个元素（如包、模块、库等）。例如，Lake 从单个模块生成 olean、ilean、c 和 o 文件，这些组件都被称为该模块的一个 facet。同样地，Lake 可以从一个库中编译静态和共享两种二进制文件。也就是说，库同时具有 static 和 shared 两种 facet。Lake 还允许用户定义自己的自定义 facet 来从模块和包构建，但这一特性当前仍在试验阶段且尚无相关文档。

trace 是用来检查目标是否最新（即是否需要重新构建）的一些数据（通常是哈希值）。如果已构建目标的 trace 与构建过程中计算的 trace 相匹配，则目标被认为是最新的。目标的 trace 源于其各种**输入**（如源文件、Lean 工具链、导入等）。

包配置选项¶

Lake 提供了多种多样的包配置选项。

布局¶

这些选项控制包及其构建目录的顶层目录布局。库、可执行文件和包内的目标指定的进一步路径相对于这些目录。

packagesDir: Lake 下载远程依赖项的目录。默认为 .lake/packages。

srcDir: 包含包的 Lean 源文件的目录。默认为包目录。

buildDir: Lake 输出包构建结果的目录。默认值为 build。

leanLibDir: Lake 输出包的二进制 Lean 库文件（如 .olean、.ilean 文件）的构建子目录。默认为 lib。

nativeLibDir: Lake 输出包的本地库文件（如 .a、.so、.dll 文件）的构建子目录。默认为 lib。

binDir: Lake 输出包的二进制可执行文件的构建子目录。默认为 bin。

irDir: Lake 输出包的中间结果（如 .c、.o 文件）的构建子目录。默认为 ir。

构建与运行¶

这些选项配置包中代码的构建和运行方式。包内的库、可执行文件和其他目标可以进一步添加到此配置的部分内容。

platformIndependent: 确定 Lake 是否应假设 Lean 模块平台无关。即，Lake 是否应在模块的 trace 中包含平台及其依赖的元素。有关更多详情，请参阅 Lake.LeanConfig.platformIndependent 的文档字符串。默认值为 none。

precompileModules: 是否将每个模块编译为本地共享库文件，该文件在模块导入时加载。这加快了元程序的评估，并允许解释器运行带有 @[extern] 标记的函数。默认值为 false。

moreServerOptions: 传递给由 lake serve 启动的 Lean 语言服务器（即 lean --server）的附加选项数组。

moreGlobalServerArgs: 传递给 lean --server 的附加参数数组，这些参数适用于此包及同一服务器会话中的其他任何内容（例如，通过 go-to-definition 在同一会话中浏览其他包时）。

buildType: 包中目标的 BuildType（参见 CMAKE_BUILD_TYPE）。可以为 debug、relWithDebInfo、minSizeRel 或 release 其中之一。默认值为 release。

leanOptions: 传递给由 lake serve 启动的 Lean 语言服务器（即 lean --server）和在编译 Lean 源文件时传递给 lean 的附加选项。

moreLeanArgs: 编译 Lean 源文件时传递给 lean 的附加参数数组。

weakLeanArgs: 编译 Lean 源文件时传递给 lean 的附加参数数组。与 moreLeanArgs 不同的是，这些参数不会影响构建结果的 trace，因此可以在不触发重构的情况下更改。在 moreLeanArgs 之前传递。

moreLeancArgs: 编译由 lean 生成的 C 源文件时传递给 leanc 的附加参数数组。Lake 已经根据 buildType 传递了一些标志，但你可以通过添加 -O0 和 -UNDEBUG 之类的参数来更改它。

weakLeancArgs: 编译由 lean 生成的 C 源文件时传递给 leanc 的附加参数数组。与 moreLeancArgs 不同的是，这些参数不会影响构建结果的 trace，因此可以在不触发重建的情况下更改。在 moreLeancArgs 之前传递。

moreLinkArgs: 链接时（例如，二进制可执行文件或共享库）传递给 leanc 的附加参数数组。这些参数将位于 extern_lib 目标的路径之后。

weakLinkArgs: 链接时（例如，二进制可执行文件或共享库）传递给 leanc 的附加参数数组。与 moreLinkArgs 不同的是，这些参数不会影响构建结果的 trace，因此可以在不触发重建的情况下更改。在 moreLinkArgs 之前传递。

extraDepTargets: 包应始终最先构建的目标名称数组。

测试与检查¶

CLI 命令 lake test 和 lake lint 使用由工作空间的根包配置的定义来执行测试和检查（这称为测试或检查 driver）。在 Lean 配置文件中，可以通过将 @[test_driver] 或 @[lint_driver] 应用于 script、lean_exe 或 lean_lib 来指定这些定义。也可以通过包中的以下选项（以 Lean 或 TOML 格式）进行配置。

testDriver: 驱动 lake test 的脚本、可执行文件或库的名称。

testDriverArgs: 传递给包的测试驱动程序的参数数组。

lintDriver: lake lint 使用的脚本或可执行文件的名称。库不能用作检查驱动程序。

lintDriverArgs: 传递给包的检查驱动程序的参数数组。

你可以使用语法 <pkg>/<name> 将依赖项中的定义指定为包的测试或检查驱动程序。可执行驱动程序将被构建然后运行，脚本驱动程序将仅运行，而库驱动程序将仅构建。脚本或可执行驱动程序会运行包配置的任何参数（例如，通过 testDriverArgs），然后是 CLI 中指定的任何参数（例如，通过 lake lint -- <args>...）。

云发布¶

这些选项为包定义云发布。详细信息参见GitHub 发布构建部分。

releaseRepo: 上传和下载此包发布版本的 GitHub 仓库 URL。如果为 none（默认），则下载时，Lake 使用包的下载 URL（如果是依赖项），上传时使用 gh 的默认 URL。

buildArchive: GitHub 云发布的构建归档名称。默认为 {(pkg-)name}-{System.Platform.target}.tar.gz。

preferReleaseBuild: 当此包用作依赖项时，是否优先下载预构建发布（从 GitHub），而不是从源码构建此包。

设定构建目标¶

一个 Lake 包可能有许多的构建目标，比如不同的 Lean 库和诸多二进制可执行文件。不论数量多少，你总可以在 @[default_target] 后声明它们，这样就可以用 lake build 轻松构建。

Lean 库¶

Lean 库目标定义了可供 import 的 Lean 模块以及它们的构建方式。

语法

lean_lib «target-name» where
  -- 配置选项从这里开始

[[lean_lib]]
name = "«target-name»"
# 更多配置选项从这里开始

配置选项

srcDir: 包目录下的子目录，包含库的源文件。默认值为包的 srcDir。（这将作为 -R 选项传递给 lean。）

roots: 库的根模块名数组。这些根模块的子模块（例如，Lib 的 Lib.Foo）被视为库的一部分。默认值为目标名的单一根。

globs: 构建库的模块 glob 数组。术语 glob 来源于 Unix 的文件 glob（例如，foo/*）。子模块 glob 构建模块目录中的每个 Lean 源文件（即， Glob.submodules `Foo 基本上等同于理论上的 import Foo.*）。glob 文件的本地导入（即工作区的其他模块）也会递归构建。默认值为库中每个 roots 的 Glob.one。

libName: 库的字符串名称。用作其静态和动态二进制文件名的基础。默认值为目标名称。

extraDepTargets: 在库模块之前构建的目标名称数组。

defaultFacets: 库的 facets 数组，用于在 lake build 中构建库。例如，将其设置为 #[LeanLib.sharedLib] 将构建共享库 facet。

nativeFacets: 一个函数 (shouldExport : Bool) → Array，确定构建并组合到库的静态和共享库中的模块 facets。如果 shouldExport 为真，模块 facets 应导出用户可能期望在库中查找的任何符号。例如，Lean 解释器将使用链接库中的导出符号。默认值为 Module.oExportFacet 的单例（如果 shouldExport）或 Module.oFacet。也就是说，从 Lean 源文件编译的目标文件，可能包含导出的 Lean 符号。

platformIndependent、precompileModules、buildType、leanOptions、<more|weak><Lean|Leanc|Link>Args、moreServerOptions：增强包的相应配置选项。库的参数紧随其后，如果库或包都预编译，则模块会被预编译，platformIndependent 在 none 情况下会回退到包，并且构建类型是两者中的最低值（debug 是最低的，而 release 是最高的）。

二进制可执行文件¶

一个 Lean 二进制可执行文件目标从带有 main 函数的 Lean 模块文件构建出可执行文件。

语法

lean_exe «target-name» where
  -- 配置选项从这里开始

[[lean_exe]]
name = "«target-name»"
# 更多配置选项从这里开始

配置选项

srcDir: 包目录下的子目录，包含可执行文件的源文件。默认值为包的 srcDir。（这将作为 -R 选项传递给 lean。）

root: 二进制可执行文件的根模块名。应包含一个 main 定义，它将作为程序的入口点。通过递归构建其本地导入（即工作区的其他模块）来构建根。默认值为目标名称。

exeName: 二进制可执行文件的字符串名称。默认值为目标名称，且其中的 . 替换为 -。

extraDepTargets: 在可执行文件模块之前构建的目标名称数组。

nativeFacets: 一个函数 (shouldExport : Bool) → Array，确定将哪些模块 facets 构建并链接到可执行文件中。如果 shouldExport 为真，模块 facets 应导出用户可能期望在库中查找的任何符号。例如，Lean 解释器将使用链接库中的导出符号。默认值为 Module.oExportFacet 的单例（如果 shouldExport）或 Module.oFacet。也就是说，从 Lean 源文件编译的目标文件，可能包含导出的 Lean 符号。

supportInterpreter: 是否将可执行文件中的符号暴露给 Lean 解释器。这允许可执行文件解释 Lean 文件（例如，通过 Lean.Elab.runFrontend）。在实现方面，在 Windows 上，Lean 共享库链接到可执行文件，其他系统上，可执行文件使用 -rdynamic 进行链接。这会增加 Linux 上二进制文件的大小，在 Windows 上，需要 libInit_shared.dll 和 libleanshared.dll 与可执行文件共同定位或作为 PATH 的一部分（例如，通过 lake exe）。因此，此功能应仅在必要时启用。默认值为 false。

platformIndependent、precompileModules、buildType、leanOptions、<more|weak><Lean|Leanc|Link>Args、moreServerOptions：增加包的相应配置选项。可执行文件的参数在库参数之后，如果库或包都预编译，则模块会被预编译，platformIndependent 在 none 情况下会回退到包，并且构建类型是两者中的最低值（debug 是最低的，而 release 是最高的）。

外部库¶

外部库目标是一个非 Lean 的**静态**库，将链接到包及其依赖项的二进制文件（例如，它们的共享库和可执行文件）。

重要: 为了在 precompileModules 开启时外部库正确链接，由 extern_lib 目标生成的静态库必须遵循平台的库命名约定（即在 Windows 上命名为 foo.a，在 Unix 上命名为 libfoo.a）。为了简化此操作，可以使用 Lake.nameToStaticLib 实用函数将库名称转换为适合平台的正确文件名称。

语法

extern_lib «target-name» (pkg : NPackage _package.name) :=
  -- 生成静态库的构建函数

该声明本质上是围绕 System.FilePath 目标的包装。类似于这样的目标，pkg 参数及其类型说明是可选的，主体应为类型 FetchM (BuildJob System.FilePath) 的函数，该函数构建静态库。pkg 参数的类型为 NPackage _package.name，以确凿地表明这是定义外部库的包。

自定义目标¶

可以通过 lake build <target-name> 构建的任意目标。

语法

target «target-name» (pkg : NPackage _package.name) : α :=
  -- 生成一个 `BuildJob α` 的构建函数

pkg 参数及其类型说明是可选的，主体应为类型 FetchM (BuildJob α) 的表达式。pkg 参数的类型为 NPackage _package.name，以确凿地表明这是定义该目标的包。

Lake 包也可以为包、模块和库定义新的 facet。定义后，新 facet（例如 facet）可以在其类型的任何当前或未来对象上构建（例如，通过 lake build pkg:facet 进行包 facet 的构建）。模块 facet 也可以提供给 LeanLib.nativeFacets 以便在生成共享库时由 Lake 自动构建和使用。

语法

package_facet «facet-name» (pkg : Package) : α :=
  -- 生成一个 `BuildJob α` 的构建函数

module_facet «facet-name» (mod : Module) : α :=
  -- 生成一个 `BuildJob α` 的构建函数

library_facet «facet-name» (lib : LeanLib) : α :=
  -- 生成一个 `BuildJob α` 的构建函数

在这些定义中，目标参数及其类型说明是可选的，主体应为类型 FetchM (BuildJob α) 的表达式。

添加依赖¶

Lake 包可添加依赖。依赖是当前包为了运行所需要的其他 Lake 包。它们可以直接来自本地文件夹（如包的子目录），也可以来自远程 Git 仓库。例如，你可以这样添加 mathlib 依赖：

package hello

require "leanprover-community" / "mathlib"

下次运行 lake build （或是用 VSCode 一类的编辑器刷新依赖）时将会克隆并构建 mathlib 仓库。克隆的特定版本的信息将存入 lake-manifest.json 以确保可复现性（即保证未来的构建使用同一版本的 mathlib）。在这之后如果想要更新 mathlib，你需要使用 lake update —— 其它的命令都将不会更新已解析的依赖。

对于依赖 mathlib 的定理证明包，你也可以用 lake new <package-name> math 直接创建带有 mathlib 依赖的包配置（且无二进制可执行文件目标）。

注意： 对于 mathlib 而言，在添加或升级其作为依赖后，你还需要在 lake build 之前使用 lake exe cache get。否则构建将从零开始（耗时数小时）。参阅 mathlib wiki 页面获取更多信息。

Lean `require`¶

Lean 的 Lake 配置文件中 require 命令的基本语法如下：

require ["<scope>" /] <pkg-name> [@ <version>]
  [from <source>] [with <options>]

from 从句告知 Lake 依赖的地址。没有 from 从句，Lake 将从默认注册表（例如 Reservoir）中查找包，并使用获得的信息下载指定 version 的包。可选的 scope 用来消除同名包的歧义。在 Reservoir 中，scope 部分是包的所有者（例如，@leanprover/doc-gen4 中的 leanprover）。

with 子句指定用于配置依赖项的 Lake 选项的 NameMap String。这相当于在命令行中将 -K 选项传递给依赖项。

受支持的源¶

在 from 子句中，Lake 支持下列依赖源。

路径依赖¶

from <path>

Lake 将从 path 目录（相对于所依赖包的目录）中加载包。

Git 依赖¶

from git <url> [@ <rev>] [/ <subDir>]

Lake 从固定的 url 中克隆 Git 仓库，并 checkout 到指定的 rev。其中 rev 可以是 commit hash、branch 或 tag。如果都没有指定，Lake 将使用默认的 master 分支。checkout 之后，Lake 将从子目录 subDir 中加载包（如果未指定子目录，则从仓库根目录加载）。

TOML `require`¶

要在 TOML 配置文件中 require 一个包，其等价语法如下：

# A Reservoir dependency
[[require]]
name = "<pkg-name>"
scope = "<scope>"
version = "<version>"
options = {<options>}

# A path dependency
[[require]]
name = "<pkg-name>"
path = "<path>"

# A Git dependency
[[require]]
name = "<pkg-name>"
git = "<url>"
rev = "<rev>"
subDir = "<subDir>"

GitHub 发布构建¶

Lake 支持将构建产物（即已归档的构建目录）上传到 GitHub 发布版本，或从中下载。这使得终端用户可以从云端获取预构建的产物，而无需自己从源码重建包。

下载¶

要下载产物，用户应配置包的选项releaseRepo? 和 buildArchive?，指向托管发布的 GitHub 仓库及其中的正确产物名称（如果默认设置不够）。然后，设置 preferReleaseBuild := true 以告知 Lake 获取并解压它作为额外的包依赖项。

Lake 仅在其标准构建过程中才会获取发布构建，如果需要的包是依赖项（因为根包通常会被修改，因此不常与此方案兼容）。然而，如果希望获取根包的发布（例如，在克隆发布的源码后但在编辑之前），可以通过 lake build :release 手动执行此操作。

Lake 内部使用 curl 下载发布，并使用 tar 解压缩它，因此终端用户必须安装这两种工具才能使用此功能。如果 Lake 由于任何原因无法获取发布，它将转而从源码构建。另外请注意，此机制在技术上不仅限于 GitHub，任何使用相同 URL 方案的 Git 主机也可以使用。

上传¶

要将构建的包作为产物上传到 GitHub 发布，Lake 提供了一个便捷的简写命令 lake upload <tag>。此命令使用 tar 将包的构建目录打包成档案，并使用 gh release upload 将其附加到 tag 对应的预先存在的 GitHub 发布版本中。因此，为了使用它，包上传者（但不是下载者）需要安装 gh，即 GitHub CLI，并将其添加到 PATH。

编写及运行脚本¶

配置文件中也可能包含 scripts 声明。脚本是任意的 (args : List String) → ScriptM UInt32 类型的定义，可以通过 lake script run 来运行。例如以下的 lakefile.lean：

import Lake
open Lake DSL

package scripts

/--
Display a greeting

USAGE:
  lake run greet [name]

Greet the entity with the given name. Otherwise, greet the whole world.
-/
script greet (args) do
  if h : 0 < args.length then
    IO.println s!"Hello, {args[0]'h}!"
  else
    IO.println "Hello, world!"
  return 0

脚本 greet 可以这样运行：

$ lake script run greet
Hello, world!
$ lake script run greet me
Hello, me!

你可以用 lake script doc 输出一个脚本的 docstring：

$ lake script doc greet
Display a greeting

USAGE:
  lake run greet [name]

Greet the entity with the given name. Otherwise, greet the whole world.

从源码构建并运行 Lake¶

如果你已经安装了带有 lake 的 Lean，可以直接用 lake build 构建一个新的 lake。

或者，你可以使用已预打包的 build.sh 脚本来构建 Lake。它将参数传递给 make 命令。所以，如果你的处理器支持多核心，可以使用 -jX 选项指定希望并行运行的构建任务数。例如：

$ ./build.sh -j4

构建后，lake 二进制文件将位于 .lake/build/bin/lake 中，而库的 .olean 文件将位于 .lake/build/lib 下。

使用 Nix Flakes 构建¶

Lake 是 Lean 4 flake 的一部分，在仓库根目录下构建。

增强 Lake 的搜索路径¶

lake 可执行文件需要知道在包配置文件中使用的模块的 Lean 库文件（例如 .olean, .ilean）在哪里（以及编辑器中 go-to-definition 支持的源文件）。Lake 将基于自身可执行文件和 lean 的位置智能地设置初始搜索路径。

具体而言，如果 Lake 与 lean 位于同一位置（即与 lake 在同一目录下有 lean 可执行文件），它将假定它是与 Lean 一起安装的，并且 Lean 和 Lake 位于其共享的 sysroot 下。具体来说，它们的二进制文件位于 <sysroot>/bin，它们的 Lean 库文件位于 <sysroot>/lib/lean，Lean 的源文件位于 <sysroot>/src/lean，而 Lake 的源文件位于 <sysroot>/src/lean/lake。否则，它将运行 lean --print-prefix 以找到 Lean 的 sysroot，并假定 Lean 的文件如前所述，而 lake 位于 <lake-home>/.lake/build/bin/lake，其 Lean 库文件位于 <lake-home>/.lake/build/lib，其源文件直接位于 <lake-home>。

可以通过在 LEAN_PATH 环境变量中包含其他 Lean 库目录（以及在 LEAN_SRC_PATH 中的源文件目录）来增强此搜索路径。这允许用户在 Lean 的文件（或 Lake 本身）位于非标准位置时更正 Lake 的搜索路径。然而，这些目录不会优先于初始搜索路径。这在开发期间很重要，因为这可以防止用于构建 Lake 的 Lake 版本使用正在构建的 Lake 版本的 Lean 库（而不是它自己的）来详细说明 Lake 的 lakefile.lean（这可能会导致各种错误）。