These are instructions to set up a working development environment for those who wish to make changes to Lean itself. It is part of the Development Guide.

We strongly suggest that new users instead follow the Quickstart to get started using Lean, since this sets up an environment that can automatically manage multiple Lean toolchain versions, which is necessary when working within the Lean ecosystem.

Requirements

Platform-Specific Setup

Generic Build Instructions

Setting up a basic parallelized release build:

git clone https://github.com/leanprover/lean4
cd lean4
cmake --preset release
make -C build/release -j$(nproc || sysctl -n hw.logicalcpu)

You can replace $(nproc || sysctl -n hw.logicalcpu) with the desired parallelism amount.

The above commands will compile the Lean library and binaries into the stage1 subfolder; see below for details.

You should not usually run cmake --install after a successful build. See Dev setup using elan on how to properly set up your editor to use the correct stage depending on the source directory.

Useful CMake Configuration Settings

Pass these along with the cmake --preset release command. There are also two alternative presets that combine some of these options you can use instead of release: debug and sandebug (sanitize + debug).

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

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

Troubleshooting

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