The Lean Language Reference

21. Build Tools and Distribution🔗

The Lean toolchain is the collection of command-line tools that are used to check proofs and compile programs in collections of Lean files. Toolchains are managed by elan, which installs toolchains as needed. Lean toolchains are designed to be self-contained, and most command-line users will never need to explicitly invoke any other than lake and elan. The contain the following tools:

lean

The Lean compiler, used to elaborate and compile a Lean source file.

lake

The Lean build tool, used to invoke incrementally invoke lean and other tools while tracking dependencies.

leanc

The C compiler that ships with Lean, which is a version of Clang.

leanmake

An implementation of the make build tool, used for compiling C dependencies.

leanchecker

A tool that replays elaboration results from .olean files through the Lean kernel, providing additional assurance that all terms were properly checked.

In addition to these build tools, toolchains contain files that are needed to build Lean code. This includes source code, .olean files, compiled libraries, C header files, and the compiled Lean run-time system. They also include external proof automation tools that are used by tactics included with Lean, such as cadical for bv_decide.

  1. 21.1. Lake
  2. 21.2. Managing Toolchains with Elan