Lean toolchain 是命令行工具的集合，用于检查 Lean 文件集合中的校样和编译程序。 工具链由 elan 管理，它根据需要安装工具链。 Lean 工具链被设计为独立的，大多数命令行用户永远不需要显式调用 lake 和 elan 以外的任何工具链。 它们包含以下工具：

lean

Lean编译器，用于细化和编译Lean源文件。

lake

Lean 构建工具，用于在跟踪依赖项的同时增量调用 lean 和其他工具。

leanc

Lean 附带的 C 编译器是 Clang 的一个版本。

leanmake

make 构建工具的实现，用于编译 C 依赖项。

leanchecker

该工具可通过 Lean内核重播 .olean 文件 中的精化结果，从而进一步确保所有条款均已正确检查。