显示活动工具链的名称和 lean 的版本。
如果安装了多个工具链，则会全部列出。
24.2. 使用 Elan 管理工具链
Elan 是 Lean 工具链管理器。 它既负责安装工具链，也负责运行工具链中的程序。 借助 Elan，可以无缝处理各种项目；每个项目都针对特定 Lean 版本进行构建，而无需手动安装和选择工具链版本。 每个项目通常配置为使用某个特定版本；该版本会按需透明地安装，而 Lean 版本的变更会自动受到跟踪。
24.2.1. 选择工具链
使用 Elan 时，PATH 中每个工具的版本都是一个调用正确版本的代理。
代理会为当前上下文确定适当的工具链版本，确保该版本已安装，然后调用相应工具链安装中的底层工具。
可以传入以 + 为前缀的参数，指示这些代理使用特定版本；因此 lake +4.0.0 会调用 4.0.0 版的 lake，必要时先安装它。
24.2.1.1. 工具链标识符
工具链通过工具链标识符指定；标识符可以是标识某类 Lean 发行版并可选带有来源的通道，也可以是由 elan toolchain link 建立的自定义工具链名称。
通道可以是：
-
stable 最新的 Lean 稳定发行版。Elan 会自动跟踪稳定发行版，并在新版本发布时提示升级。
-
beta 最新的候选发行版。候选发行版是计划成为下一个稳定发行版的 Lean 构建，供广大用户测试。
-
nightly 最新的每夜构建。每夜构建适合试用 Lean 的新功能并向开发者提供反馈。
- 版本号或特定的每夜发行版
每个 Lean 版本号都标识一个仅包含该发行版的通道。 版本号前可以带有
v，因此v4.17.0与4.17.0等价。 类似地，nightly-YYYY-MM-DD指定相应日期的每夜发行版。 项目的工具链文件通常应包含具体的 Lean 版本，而不是宽泛的通道，以便开发者相互协调，并构建和测试项目的旧版本。 Lean 发行版和每夜构建有一份持续维护的归档。- 自定义本地工具链
可以使用
elan toolchain link命令，在 Elan 中为 Lean 的本地构建建立自定义工具链名称。 这在开发 Lean 编译器本身时尤其有用。
指定来源会指示 Elan 从特定源安装 Lean 工具链。
默认情况下，这是 GitHub 上标识为 leanprover/lean4 的官方项目仓库。
如果指定来源，它应位于通道之前，并用冒号分隔，因此 stable 等价于 leanprover/lean4:stable。
安装每夜发行版时，会向来源追加 -nightly，因此 leanprover/lean4:nightly-2025-03-25 会查询 leanprover/lean4-nightly 仓库以下载发行版。
自定义工具链名称不使用来源。
24.2.1.2. 确定当前工具链
Elan 将工具链与目录关联，并使用当前工作目录向上最近的、已配置工具链的父目录所对应的工具链。
目录的工具链可能来自工具链文件，也可能来自使用 elan override 配置的覆盖项。
确定当前工具链时，首先查找为当前目录配置的工具链，然后逐级向上检查父目录，直到找到工具链版本或不再有父目录。
若某目录配置了工具链覆盖项，或包含 lean-toolchain 文件，则该目录已配置工具链。
较近的父目录优先于其祖先目录；如果一个目录同时有覆盖项和工具链文件，则覆盖项优先。
如果没有找到目录工具链，则以 Elan 配置的默认工具链作为后备。
配置 Lean 工具链最常见的方式是使用工具链文件。
工具链文件是名为 lean-toolchain 的文本文件，其中只有一行有效的工具链标识符。
该文件通常位于项目根目录，并与代码一同纳入版本控制，确保项目的所有开发者使用相同版本。
更新到新的 Lean 工具链只需编辑此文件；下次打开或构建 Lean 文件时，新版本便会自动下载并运行。
在某些需要更大灵活性的高级用例中，可以配置工具链覆盖项。 与工具链文件一样，覆盖项将工具链版本与某个目录及其子目录关联。 与工具链文件不同，覆盖项存储在 Elan 的配置中，而不是本地文件中。 它们通常用于需要不适合其他开发者的特定本地配置时，例如使用本地构建的 Lean 编译器测试项目。
24.2.2. 工具链位置
默认情况下，Elan 将已安装的工具链存储在用户主目录的 .elan/toolchains 中，其代理则保存在 .elan/bin 中；安装 Elan 时会将后者添加到路径。
可以使用环境变量 ELAN_HOME 更改此位置。
为确保能找到 Elan 的文件，应在安装 Elan 之前以及所有使用 Lean 的会话中设置它。
24.2.3. 命令行界面
除了自动选择、安装并调用正确版本 Lean 工具的代理外，Elan 还提供用于查询和配置其设置的命令行界面。
该工具名为 elan。
与 Lake 类似，其命令行界面围绕子命令组织。
调用 Elan 时可以使用以下标志：
-
--help或-h 详细说明当前子命令。
-
--verbose或-v 启用详细输出。
-
--version或-V 显示 Elan 版本。
24.2.3.1. 查询工具链
elan show 命令显示当前工具链（由当前目录确定），并列出所有已安装的工具链。
Elan command
elan show
下面是在含有 lean-toolchain 文件的项目中运行 elan show 的典型输出：
installed toolchains -------------------- leanprover/lean4:nightly-2025-03-25 leanprover/lean4:v4.17.0 (resolved from default 'stable') leanprover/lean4:v4.16.0 leanprover/lean4:v4.9.0 active toolchain ---------------- leanprover/lean4:v4.9.0 (overridden by '/PATH/TO/PROJECT/lean-toolchain') Lean (version 4.9.0, arm64-apple-darwin23.5.0, commit 8f9843a4a5fe, Release)
installed toolchains 一节列出系统上当前可用的所有工具链。
active toolchain 一节标识当前工具链，并说明其选择方式。
在此例中，工具链是根据 lean-toolchain 文件选择的。
24.2.3.2. 设置默认工具链
Elan 的配置文件指定一个默认工具链，在当前目录没有 lean-toolchain 文件或工具链覆盖项时使用。
通常使用 elan default 命令更改此值，而不是手动编辑该文件。
24.2.3.3. 管理已安装的工具链
elan toolchain 子命令族用于管理已安装的工具链。
工具链存储在 Elan 的工具链目录中。
已安装的工具链可能占用大量磁盘空间。
Elan 会跟踪曾在其中调用过它的 Lean 项目，并保存一份列表。
这份项目列表可用于确定哪些工具链正在使用，并通过 elan toolchain gc 自动删除未使用的工具链版本。
Elan command
elan toolchain uninstall toolchain
卸载指定的 toolchain。
工具链名称应为某个已安装工具链的名称。
使用 elan toolchain list 查看已安装工具链及其名称。
Elan command
elan toolchain link local-name path
使用在 path 处找到的 Lean 工具链，创建名为 local-name 的新本地工具链。
Elan command
elan toolchain gc [--delete] [--json]
此命令目前仍被视为实验性命令。
确定已安装工具链中哪些正在使用，并提议删除未使用的工具链。 所有已安装的工具链都会列出，并分成正在使用和未使用两类。
如果满足以下条件，工具链会被归类为“正在使用”：
-
它是默认工具链；
-
它被注册为覆盖项；或者
-
某目录的
lean-toolchain文件引用了该工具链，并且此前曾在该目录中使用过 elan。
出于安全考虑，除非传入 --delete 标志，否则 elan toolchain gc 不会实际删除任何工具链。
将来当实现被认为足够成熟时，可能会放宽这一要求。
--json 标志使 elan toolchain gc 以适合其他工具处理的 JSON 格式输出已使用和未使用工具链的列表。
24.2.3.4. 管理目录覆盖项
目录专属的工具链覆盖项是一种优先于 lean-toolchain 文件的本地配置。
elan override 命令用于管理覆盖项。
Elan command
elan override list
以两列列出当前配置的所有目录覆盖项。 左列包含 Lean 版本被覆盖的目录，右列列出工具链版本。
Elan command
elan override set toolchain
将 toolchain 设置为当前目录的覆盖项。
Elan command
elan override unset [--nonexistent] [--path path]
如果提供 --nonexistent 标志，则移除为当前不存在的目录配置的所有覆盖项。
如果提供 --path，则移除为 path 设置的覆盖项。
否则，移除当前目录的覆盖项。
24.2.3.5. 运行工具和命令
本节中的命令可在指定工具链中运行命令，并可在磁盘上定位特定工具链中的工具。 这适用于试验不同 Lean 版本、进行跨版本测试以及将 Elan 与其他工具集成。
Elan command
elan run [--install] toolchain command ...
配置环境以使用给定工具链，然后运行指定程序。
如果提供 --install 标志，则会安装该工具链。
该命令可以是任何程序，不必是 lean 或 lake 之类工具链中的命令。
这样无需设置覆盖项即可测试任意工具链。
Elan command
elan which command
显示 command 在该工具链中对应二进制文件的完整路径。
24.2.3.6. 管理 Elan
Elan 可以管理自身的安装。 它可以自行升级、自行卸载，并帮助为许多常用命令外壳配置制表符补全。
Elan command
elan self update
下载并安装 Elan 自身的更新。
Elan command
elan self uninstall
卸载 Elan。
Elan command
elan completions shell
为 Elan 生成命令外壳补全脚本，从而在多种命令外壳中启用 Elan 命令的制表符补全。
有关安装方法的说明，请参阅 elan help completions 的输出。