显示活动工具链的名称和 lean 的版本。
如果安装了多个工具链，则会列出它们。
24.2. 使用Elan管理工具链
Elan 是 Lean 工具链经理。 它负责安装 工具链 并运行其组成程序。 Elan 可以无缝地处理各种项目，每个项目都设计为使用特定版本的 Lean 构建，而无需手动安装和选择工具链版本。 每个项目通常配置为使用特定版本，该版本根据需要透明安装，并自动跟踪对 Lean 版本的更改。
24.2.1. 选择工具链
使用Elan时，PATH上每个工具的版本是调用正确版本的代理。
代理确定当前上下文的适当工具链版本，确保其已安装，然后调用适当工具链安装中的底层工具。
可以通过将特定版本作为前缀为 + 的参数传递来指示这些代理使用特定版本，以便 lake +4.0.0 在安装后调用 lake 版本 4.0.0（如有必要）。
24.2.1.1. 工具链标识符
工具链是通过提供工具链标识符来指定的，该标识符可以是 channel（标识特定类型的 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 编译器本身时特别有用。
指定 origin 指示 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 配置的 default toolchain 作为后备。
配置 Lean 工具链的最常见方法是使用 toolchain file。
工具链文件是一个名为 lean-toolchain 的文本文件，其中包含带有有效 工具链标识符 的单行。
该文件通常位于项目的根目录中，并通过代码签入版本控制，以确保参与该项目的每个人都使用相同的版本。
更新到新的 Lean 工具链只需编辑此文件，新版本会在下次打开或构建 Lean 文件时自动下载并运行。
在某些需要更大灵活性的高级用例中，可以配置 toolchain override。 与工具链文件一样，覆盖将工具链版本与目录及其子目录相关联。 与工具链文件不同，覆盖存储在 Elan 的配置中而不是本地文件中。 它们通常在需要特定的本地配置且对其他开发人员来说没有意义时使用，例如使用本地构建的 Lean 编译器测试项目。
24.2.2. 工具链位置
默认情况下，Elan 将安装的工具链存储在用户主目录的 .elan/toolchains 中，其代理保存在 .elan/bin 中，该代理在安装 Elan 时添加到路径中。
环境变量 ELAN_HOME 可用于更改此位置。
应在安装 Elan 之前和使用 Lean 的所有会话中进行设置，以确保找到 Elan 的文件。
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 install toolchain
安装指示的 toolchain。
工具链的名称应为 适合包含在 lean-toolchain 文件中的标识符。
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 之前已在该目录中使用过。
出于安全原因，elan toolchain gc 实际上不会删除任何工具链，除非传递了 --delete 标志。
当未来认为实施足够成熟时，这一点可能会放宽。
--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 可以管理自己的安装。 它可以自我升级、自我删除，并帮助为许多流行的 shell 配置制表符完成。
Elan command
elan self update
下载并安装 Elan 本身的更新。
Elan command
elan self uninstall
卸载 Elan。
Elan command
elan completions shell
为 Elan 生成 shell 完成脚本，从而在各种 shell 中为 Elan 命令启用制表符完成。
有关如何安装它们的说明，请参阅 elan help completions 的输出。