lean4-htt/doc/make/index.md

Requirements

• C++14 compatible compiler
• CMake
• GMP (GNU multiprecision library)

Platform-Specific Setup

• Linux (Ubuntu)
• Windows (msys2)
• Windows (Visual Studio)
• macOS (homebrew)
• Linux/macOS/WSL via Nix: Call nix-shell in the project root. That's it.

Generic Build Instructions

Setting up a basic release build:

git clone https://github.com/leanprover/lean4
cd lean
mkdir -p build/release
cd build/release
cmake ../..
make

Setting up a basic debug build:

git clone https://github.com/leanprover/lean4
cd lean
mkdir -p build/debug
cd build/debug
cmake -D CMAKE_BUILD_TYPE=DEBUG ../..
make

This will compile the Lean library and binary into the stage0.5 subfolder; see below for details. Add -jN for an appropriate N to make for a parallel build.

Useful CMake Configuration Settings

Pass these along with the cmake ../.. command.

• -D CMAKE_BUILD_TYPE=
  Select the build type. Valid values are RELEASE (default), DEBUG, RELWITHDEBINFO, and MINSIZEREL.

• -D CMAKE_C_COMPILER=
-D CMAKE_CXX_COMPILER=
  Select the C/C++ compilers to use. Official Lean releases currently use Clang; see also .github/workflows/ci.yml for the CI config.

• -D CHECK_OLEAN_VERSION=OFF
  The .olean files are tagged with the Lean version they were produced with. This means that by default, the core library has to be recompiled after e.g. every git commit. Use this option to avoid the version check. The .olean files can be removed manually by invoking make clean-olean.

Lean will automatically use CCache if available to avoid redundant builds, especially after stage 0 has been updated (see below).

Lean Build Pipeline

Since version 4, Lean is a partially bootstrapped program: most parts of the frontend and compiler are written in Lean itself and thus need to be built before building Lean itself - which is needed to again build those parts. This cycle is broken by using pre-built C files checked into the repository (which ultimately go back to a point where the Lean compiler was not written in Lean) in place of these Lean inputs and then compiling everything in multiple stages up to a fixed point. The build directory is organized in these stages:

stage0/
  bin/
    lean  # the Lean compiler & server
    leanc  # a wrapper around a C compiler supplying search paths etc
    leanmake  # a wrapper around `make` supplying the Makefile below
  lib/
    lean/**/*.olean  # the Lean library (incl. the compiler) compiled by `lean` above
    temp/**/*.{c,o}  # the library extracted to C and compiled by `leanc`
    libInit.a  # a static library of the Lean library
    libleancpp.a  # a static library of the C++ sources of Lean
  include/
    config.h  # config variables used to build `lean` such as use allocator
    runtime/lean.h  # runtime headers, used by extracted C code, uses `config.h`
  share/lean/
    Makefile  # used by `leanmake`
stage1/...
stage2/...
stage3/...

The build for each stage starts by assembling bin/lean from the libInit.a of the preceding stage and libleancpp.a built from src/; in the case of stage 0, which doesn't have a preceding stage, both libraries are instead assembled from stage0/src, which contains the C++ and extracted C code of a previous commit of Lean. This Lean binary is then used to compile the Lean library into .olean files and ultimately a new libInit.a, which is then used by the next stage.

Each stage can be built by calling make stageN in the root build folder. It is usually not necessary to compile all stages in order to test a change. Stage 3 in fact should usually be identical to stage 2 and only exists as a sanity check, which can be done via make check-stage3. Building stage 2 should only be necessary for testing how changes in the compiler influence compilation of the compiler itself, e.g. checking if an optimization speeds up (or breaks) the compiler. Stage 1 is sufficient for testing changes on the library and test programs. In fact, if the stage 0 library and the stage 1 are compatible (use the same Lean ABI, so to speak), we can avoid even rebuilding the stage 1 library using a special stage "0.5" that combines the stage 1 compiler with the stage 0 library. Most changes do not break this ABI, so running make by itself in the root build folder will default to make stage0.5. In summary, doing a standard build via make involves these steps:

1. compile the stage0/src archived sources into stage0/bin/lean
2. use it to compile the library (including your changes) into stage0/lib
3. link that and the current C++ code from src/ into stage1/bin/lean
4. copy ("uplift") the Lean library from stage0/lib into stage1/lib

You now have a Lean binary and library that include your changes, though their own compilation was not influenced by them, that you can use to test your changes on test programs whose compilation will be influenced by the changes.

Finally, when we want to use new language features in the library, we need to update the stage 0 compiler, which can be done via make -C stageN update-stage0. Note: you cannot do this for stage 0.5 because the extracted C files are not copied over from stage 0 to that stage, so just use stage 0 instead. make update-stage0 without -C defaults to stage0 for this reason. If updating stage 0 from stage 0 sounds wrong to you, just remember that the stage 0 build directory contains the output of the stage 0 compiler!

Development Setup

After building a stage, you can invoke make -C stageN test (or, even better, make -C stageN ARGS=-j to make ctest parallel) to run the Lean test suite. make test without -C defaults to stage 0.5. While the Lean tests will automatically use that stage's corresponding Lean executables, for running tests or compiling Lean programs manually, you need to put them into your PATH yourself. A simple option for doing that is to use elan, see the next section.

The only currently supported editor is Emacs, see lean4-mode/README.md for basic setup. You can set lean4-rootdir manually to tell it what stage to use:

# while editing the Lean library
M-x set-variable lean4-rootdir RET ".../build/release/stage0" RET
# while testing, using a Lean that includes your changes
M-x set-variable lean4-rootdir RET ".../build/release/stage0.5" RET

but elan again makes it simple to do that automatically, see below.

Dev setup using elan

You can use elan to easily switch between stages and build configurations based on the current directory, both for the lean/leanc/leanmake binaries in your shell's PATH and inside Emacs.

If you haven't already installed elan, you can do so, without installing a default version of Lean, using

curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none

You can use elan toolchain link to give a specific stage build directory a reference name, then use elan override set to associate such a name to the current directory. We usually want to use stage0 for editing files in src and stage0.5 for everything else (e.g. tests).

# in the Lean rootdir
elan toolchain link lean4 build/release/stage0.5
elan toolchain link lean4-stage0 build/release/stage0
# make `lean` etc. point to stage0.5 in the rootdir and subdirs
elan override set lean4
cd src
# make `lean` etc. point to stage0 anywhere inside `src`
elan override set lean4-stage0

You can also use the +toolchain shorthand (e.g. lean +lean4-debug) to switch toolchains on the spot. lean4-mode will automatically use the lean executable associated with the directory of the current file as long as lean4-rootdir is unset and ~/.elan/bin is in your exec-path. Where Emacs sources the exec-path from can be a bit unclear depending on your configuration, so alternatively you can also set lean4-rootdir to "~/.elan" explicitly.

You might find that debugging through elan, e.g. via gdb lean, disables some things like symbol autocompletion because at first only the elan proxy binary is loaded. You can instead pass the explicit path to bin/lean in your build folder to gdb, or use gdb $(elan which lean).

Troubleshooting

• Call make with an additional VERBOSE=1 argument to print executed commands.