- C++14 compatible compiler
- GMP (GNU multiprecision library)
- Linux (Ubuntu)
- Windows (msys2)
- Windows (Visual Studio)
- Windows (WSL)
- macOS (homebrew)
- Linux/macOS/WSL via Nix: Call
nix-shellin the project root. That's it.
- There is also an experimental setup based purely on Nix that works fundamentally differently from the make/CMake setup described on this page.
Generic Build Instructions
Setting up a basic release build:
git clone https://github.com/leanprover/lean4 --recurse-submodules cd lean4 mkdir -p build/release cd build/release cmake ../.. make
For regular development, we recommend running
git config submodule.recurse true
in the checkout so that
--recurse-submodules doesn't have to be
The above commands will compile the Lean library and binaries into the
stage1 subfolder; see below for details. Add
-j N for an
make for a parallel build.
For example, on an AMD Ryzen 9
make takes 00:04:55, whereas
make -j 10
takes 00:01:38. Your results may vary depending on the speed of your hard
You should not usually run
make 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 ../.. command.
Select the build type. Valid values are
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.
makewith an additional
VERBOSE=1argument to print executed commands.