index.md

Requirements

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

Platform-Specific Setup

• Linux (Ubuntu)
• Windows (msys2)
• Windows (Visual Studio)
• macOS

Generic Build Instructions

Setting up a basic release build using make:

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

Setting up a basic debug build using make:

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

Useful CMake Configuration Settings

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

• -G Ninja CMake 2.8.11 supports the Ninja build system. Some people report that using Ninja can reduce the build time, esp when a build is incremental. Call ninja instead of make to build the project.

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

• -D CMAKE_CXX_COMPILER= Select the C++ compiler to use.

• -D LEAN_IGNORE_OLEAN_VERSION 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/ninja clean-olean.

Further Information

• Using CCache to avoid recompilation
• Measuring Code Coverage
• Compiling Lean with Split Stacks