Build Lean 4 from Source on Linux, macOS, and Windows

Building Lean 4 from source gives you full control over the compiler, lets you test local patches, and is a prerequisite for contributing to the project. These instructions are for people who want to change Lean itself. If you just want to use Lean, follow the official installation instructions instead, which use elan to manage versioned toolchains automatically.

Prerequisites

Every platform requires:

Requirement	Notes
C++14-compatible compiler	Clang is recommended; GCC works too
CMake ≥ 3.10	Used to configure and build
GMP	GNU multiprecision library
LibUV	Async I/O, used by the language server
OpenSSL	Required for HTTPS downloads in Lake

CCache is strongly recommended. Lean’s build system detects it automatically and uses it to cache compiled C files, dramatically reducing rebuild times after stage0 is updated.

Platform-Specific Setup

Ubuntu / Debian
macOS (Homebrew)
Windows (msys2)
Windows (WSL)
Nix

Install all dependencies with a single command:

sudo apt-get install \
  git libgmp-dev libuv1-dev libssl-dev \
  cmake ccache clang pkgconf

Then proceed to Generic Build Instructions.

Apple’s bundled clang++ is sufficient and recommended. Install the remaining dependencies via Homebrew:

brew install cmake gmp libuv openssl pkgconf
brew install ccache   # recommended

To use a Homebrew-installed Clang or GCC instead of Apple’s default, pass the compiler path to CMake:

cmake --preset release \
  -DCMAKE_C_COMPILER=/opt/homebrew/opt/llvm/bin/clang \
  -DCMAKE_CXX_COMPILER=/opt/homebrew/opt/llvm/bin/clang++

Then proceed to Generic Build Instructions.

Download and install MSYS2. Open the MSYS2 CLANG64 shell (not MSYS or MINGW64) and install all dependencies:

pacman -S make python \
  mingw-w64-clang-x86_64-cmake \
  mingw-w64-clang-x86_64-clang \
  mingw-w64-clang-x86_64-ccache \
  mingw-w64-clang-x86_64-libuv \
  mingw-w64-clang-x86_64-gmp \
  mingw-w64-clang-x86_64-openssl \
  git unzip diffutils binutils

When running CMake, you must specify Clang explicitly:

cmake --preset release \
  -DCMAKE_C_COMPILER=clang \
  -DCMAKE_CXX_COMPILER=clang++

Activate Developer Mode (Settings → Update & Security → For developers) before building. This enables symlink creation, which Lean uses to wire up go-to-definition in the standard library.

Windows Subsystem for Linux (WSL 2 recommended) lets you build a Linux Lean binary while editing with VS Code on Windows.

Install WSL 2 with Ubuntu and follow the Ubuntu tab above to install dependencies.
Install VS Code on Windows with the Remote Development extension.
Install the Lean 4 extension into WSL using the “Install in WSL: Ubuntu” option.
Open your repository with Ctrl+Shift+P → Remote-WSL: Open Folder in WSL.

Then proceed to Generic Build Instructions inside WSL.

Lean 4 ships a flake.nix. Enter the development shell and all dependencies are provided automatically:

git clone https://github.com/leanprover/lean4
cd lean4
nix develop

From inside the Nix shell, run the Generic Build Instructions as usual. The Nix shell uses LLVM/Clang from llvmPackages_19 and includes cmake, gmp, libuv, ccache, pkg-config, and openssl.

Generic Build Instructions

Clone the repository

git clone https://github.com/leanprover/lean4
cd lean4

Configure with a CMake preset

Choose a preset based on your goal:

Preset	Description	Output dir
`release`	Optimized build, stripped binaries	`build/release`
`dev-release`	Optimized + debug symbols (`-g3`), warnings as info	`build/release`
`debug`	`CMAKE_BUILD_TYPE=Debug`, large stack, full symbols	`build/debug`
`sandebug`	Sanitize + debug (AddressSanitizer, UBSan)	`build/sandebug`

For everyday development, dev-release is recommended:

cmake --preset dev-release

For a clean release (CI / distribution):

cmake --preset release

Build

make -C build/release -j$(nproc || sysctl -n hw.logicalcpu)

Replace the parallelism expression with an explicit number if you prefer, e.g. -j8. The build produces stage0/ and stage1/ subdirectories inside build/release/.

Verify the build

./build/release/stage1/bin/lean --version

If a make invocation fails and you want to see the exact compiler commands being run, add VERBOSE=1:

make -C build/release VERBOSE=1

CMake Configuration Options

Pass any of these alongside cmake --preset <name>:

cmake --preset release \
  -DCMAKE_BUILD_TYPE=RELEASE \
  -DCMAKE_C_COMPILER=clang \
  -DCMAKE_CXX_COMPILER=clang++

Option	Valid values	Default
`CMAKE_BUILD_TYPE`	`RELEASE`, `DEBUG`, `RELWITHDEBINFO`, `MINSIZEREL`	`RELEASE`
`CMAKE_C_COMPILER`	path to C compiler	system default
`CMAKE_CXX_COMPILER`	path to C++ compiler	system default
`STRIP_BINARIES`	`ON` / `OFF`	`OFF` in dev presets
`WFAIL`	`ON` / `OFF` — treat warnings as errors	`ON` in `release`

Official Lean releases are built with Clang. CI configuration is in .github/workflows/ci.yml.

Build Output Structure

After a successful build, the build/release/ directory contains:

stage0/
  bin/lean          # bootstrap compiler built from stage0/src/ (C sources)

stage1/
  bin/
    lean            # the Lean compiler and language server
    leanc           # wrapper around the C compiler with Lean search paths
    leanmake        # wrapper around make supplying lean.mk
  include/
    lean/
      lean.h          # runtime header for FFI consumers (#include <lean/lean.h>)
      config.h        # compile-time configuration variables
      version.h       # version information
  lib/
    lean/**/*.olean         # compiled Lean library (stdlib + compiler)
    temp/**/*.{c,o}         # C code extracted from Lean sources
    libInit.a libLean.a     # static libraries
    libleancpp.a            # C++ runtime and builtins
    libleanshared.so        # dynamic library bundling the above

stage2/  # sanity-check stage, should equal stage1
stage3/  # further sanity check

Running make alone builds through stage1, which is sufficient for testing changes on external files. Stage 2 and 3 are needed to verify that compiler changes are self-consistent. See the Development Workflow page for details on the bootstrapping pipeline.

CCache Integration

Lean’s build system detects and uses CCache automatically when it is on your PATH. CCache caches compiled C files and is especially useful after a stage0 update, where all the extracted C files must be recompiled but are identical to those from a recent build. Verify that CCache is active:

ccache --show-stats

Building Additional Stages

# Build stage1 (default)
make -C build/release

# Build stage2 (needed when .olean format changes)
make -C build/release stage2

# Build stage3 (sanity check)
make -C build/release stage3

Development

Documentation Index

​Prerequisites

​Platform-Specific Setup

​Generic Build Instructions

​CMake Configuration Options

​Build Output Structure

​CCache Integration

​Building Additional Stages

Build docs developers (and LLMs) love

Prerequisites

Platform-Specific Setup

Generic Build Instructions

CMake Configuration Options

Build Output Structure

CCache Integration

Building Additional Stages