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.
- C++14 compatible compiler
- CMake
- GMP (GNU multiprecision library)
- LibUV
- Linux (Ubuntu)
- Windows (msys2)
- Windows (WSL)
- macOS (homebrew)
- Linux/macOS/WSL via Nix: Call
nix developin the project root. That's it.
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.
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 areRELEASE(default),DEBUG,RELWITHDEBINFO, andMINSIZEREL. -
-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.ymlfor the CI config.
Lean will automatically use CCache if available to avoid redundant builds, especially after stage 0 has been updated.
- Call
makewith an additionalVERBOSE=1argument to print executed commands.