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. They contain the following tools:

lean

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

lake

The Lean build tool, used to 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.