17. 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.

When using Elan, the version of each tool on the PATH is a proxy that invokes the correct version. The proxy determines the appropriate toolchain version for the current context, ensures that it is installed, and then invokes the underlying tool in the appropriate toolchain installation. These proxies can be instructed to use a specific version by passing it as an argument prefixed with +, so lake +4.0.0 invokes lake version 4.0.0, after installing it if necessary. If present, a toolchain file in a directory causes a particular version of Lean to be used in it and all subdirectories. This file should indicate a specific version, such as leanprover/lean4:v4.15.0, leanprover/lean4:v4.16.0-rc2, or leanprover/lean4:nightly-2025-01-19. If no toolchain file is present, then the elan configuration is used to select a version to invoke. Link to Elan chapter here

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. 17.1. Lake
    1. 17.1.1. Concepts and Terminology
      1. 17.1.1.1. Builds
      2. 17.1.1.2. Facets
      3. 17.1.1.3. Scripts
      4. 17.1.1.4. Test and Lint Drivers
      5. 17.1.1.5. GitHub Release Builds
        1. 17.1.1.5.1. Downloading
        2. 17.1.1.5.2. Uploading
    2. 17.1.2. Command-Line Interface
      1. 17.1.2.1. Environment Variables
      2. 17.1.2.2. Options
      3. 17.1.2.3. Controlling Output
      4. 17.1.2.4. Automatic Toolchain Updates
      5. 17.1.2.5. Creating Packages
      6. 17.1.2.6. Building and Running
      7. 17.1.2.7. Development Tools
        1. 17.1.2.7.1. Tests and Linters
        2. 17.1.2.7.2. Scripts
        3. 17.1.2.7.3. Language Server
      8. 17.1.2.8. Dependency Management
      9. 17.1.2.9. Packaging and Distribution
        1. 17.1.2.9.1. Cached Cloud Builds
      10. 17.1.2.10. Configuration Files
    3. 17.1.3. Configuration File Format
      1. 17.1.3.1. Declarative TOML Format
        1. 17.1.3.1.1. Package Configuration
        2. 17.1.3.1.2. Dependencies
        3. 17.1.3.1.3. Library Targets
        4. 17.1.3.1.4. Executable Targets
      2. 17.1.3.2. Lean Format
        1. 17.1.3.2.1. Declarative Fields
        2. 17.1.3.2.2. Packages
        3. 17.1.3.2.3. Dependencies
        4. 17.1.3.2.4. Targets
          1. 17.1.3.2.4.1. Libraries
          2. 17.1.3.2.4.2. Executables
          3. 17.1.3.2.4.3. External Libraries
          4. 17.1.3.2.4.4. Custom Targets
          5. 17.1.3.2.4.5. Custom Facets
        5. 17.1.3.2.5. Configuration Value Types
        6. 17.1.3.2.6. Scripts
        7. 17.1.3.2.7. Utilities
    4. 17.1.4. Script API Reference
      1. 17.1.4.1. Accessing the Environment
        1. 17.1.4.1.1. Search Path Helpers
        2. 17.1.4.1.2. Elan Install Helpers
        3. 17.1.4.1.3. Lean Install Helpers
        4. 17.1.4.1.4. Lake Install Helpers
      2. 17.1.4.2. Accessing the Workspace
  2. 17.2. Reservoir