Lean 4 Development Workflow: Editor Setup and Testing

After building Lean from source, the next step is wiring up your editor so it uses the freshly built stage1 binary when you edit files inside the Lean repository. This page walks through the full development cycle: editor setup, the bootstrapping pipeline, the test suite, the commit convention, and debugging.

Setting Up Your Editor with elan

elan is Lean’s toolchain manager. It reads lean-toolchain files in directories to know which binary to invoke for lean, leanc, and leanmake. The Lean 4 repository contains two such files:

Files under src/ use the lean4-stage0 toolchain (the bootstrap compiler).
Files under tests/ use the lean4 toolchain (the stage1 output).

Run the following two commands once after your first successful build to create named toolchain links:

# In the Lean repository root
elan toolchain link lean4        build/release/stage1
elan toolchain link lean4-stage0 build/release/stage0

From that point on, opening any file in src/ from VS Code or Emacs will automatically use stage0/bin/lean for elaboration, and any file in tests/ will use stage1/bin/lean.

Install elan without a default toolchain if you do not want to affect your system-wide Lean setup:

# Unix
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \
  -sSf | sh -s -- --default-toolchain none

Switching toolchains on the fly

Use the +toolchain prefix for one-off invocations:

lean +lean4-debug --version

For debugging via GDB, pass the explicit path rather than going through the elan proxy — the proxy is a thin dispatcher and can suppress symbol autocompletion:

gdb $(elan which lean)
# or directly:
gdb build/release/stage1/bin/lean

VS Code setup

The repository ships a .vscode/ directory with pre-configured settings, recommended extensions, and build tasks. Simply open the repository root:

code .

After rebuilding lean you can reload the server inside VS Code:

Refresh File Dependencies — reloads the worker for the current file. Use this after most changes (does not require restarting the watchdog).
Restart Server — restarts both the watchdog and all workers. Use this after changing watchdog code or updating stage0.

The Bootstrapping Pipeline

Lean is a bootstrapped compiler: the frontend, elaborator, and compiler backend are written in Lean itself. This creates a chicken-and-egg dependency that is broken using pre-built C sources checked into stage0/src/.

The three-stage build

stage0/src/  (archived C files)
     │  compile with system C++ compiler
     ▼
stage0/bin/lean   ← bootstrap compiler

stage0/bin/lean  +  src/  (current Lean sources)
     │  elaborate + compile to C
     ▼
stage1/lib/*.olean  +  stage1/lib/temp/*.c

stage0/bin/lean (compiled C)  +  stage1 lib + C++ runtime
     │  link
     ▼
stage1/bin/lean   ← your development compiler

stage1/bin/lean contains your changes but was compiled by stage0, so its own compilation was not influenced by them. This means:

Changes to the elaborator, parser, or tactic system are exercised when stage1 compiles files in tests/. The stage1 compiler itself is not self-hosting your changes yet.
Changes that affect the compiled output (.olean format, code generator) may require stage2 to be fully tested, since stage2 is compiled by stage1 and both builds and expects the new format.

make -C build/release         # builds stage1 (default)
make -C build/release stage2  # builds stage2
make -C build/release stage3  # sanity check: stage3 should equal stage2

When to update stage0

stage0 must be updated when you want to use new language features (syntax, tactics, library functions) inside the compiler source itself. The update process is automated by CI:

Modify stage0/src/stdlib_flags.h (e.g., add or change a comment) to signal that stage0 is out of date.
Push to your branch. The update-stage0 GitHub Actions workflow runs automatically when src/stdlib_flags.h and stage0/src/stdlib_flags.h are out of sync.

To trigger the update manually if you have repository write access:

gh workflow run update-stage0.yml

To do it locally:

make -C build/release update-stage0-commit

PRs that contain manual changes to stage0/ (other than stdlib_flags.h) are blocked from the merge queue by CI and are labelled changes-stage0. They must use rebase merge (bypassing squash) to preserve the separate stage0 update commit. Coordinate with admins before merging such PRs.

CCache during development

Lean’s build system uses CCache automatically when available. Without it, every stage0 update triggers a full recompile of all extracted C files. Install CCache and make sure it is on your PATH:

ccache --show-stats  # verify it is active

The `prelude` keyword

All Lean submodules start with the prelude keyword, which disables the automatic import Init. This means each file must explicitly import whatever subset of Init it needs. The benefit is that editing a file in Init does not trigger a full rebuild of the entire Lean module tree.

Testing

Running the full test suite

CTEST_PARALLEL_LEVEL="$(nproc)" CTEST_OUTPUT_ON_FAILURE=1 \
  make -C build/release -j "$(nproc)" test

Re-run only the tests that failed in the previous run:

CTEST_PARALLEL_LEVEL="$(nproc)" CTEST_OUTPUT_ON_FAILURE=1 \
  make -C build/release -j "$(nproc)" test ARGS="--rerun-failed"

Running a specific test

# By regex
CTEST_PARALLEL_LEVEL="$(nproc)" CTEST_OUTPUT_ON_FAILURE=1 \
  make -C build/release -j "$(nproc)" test ARGS="-R 'tests/elab/myTest'"

# Manually without ctest
tests/with_stage1_test_env.sh path/to/test/directory/run_test.sh

Test suite layout

The tests/ directory uses two conventions:

Test directory: a directory containing run_test.sh. The script is run once with the test directory as the working directory.
Test pile: a directory with run_test.sh where each .lean file is a separate test. The script is run once per file.

Key subdirectories:

Directory	What it tests
`tests/elab/`	Elaboration output (expect exit 0)
`tests/elab_fail/`	Elaboration that should fail (expect exit 1)
`tests/compile/`	Compiled executables, checks stdout
`tests/server/`	LSP server requests
`tests/lake/`	Lake build system
`tests/pkg/`	Tests that run inside a Lake package

Testing against Mathlib

To check that your PR does not break Mathlib, rebase your branch onto nightly-with-mathlib:

git fetch origin nightly-with-mathlib
git rebase origin/nightly-with-mathlib

CI will build a lean-pr-testing-NNNN branch in leanprover-community/mathlib4-nightly-testing and report results back to your PR.

Commit Convention

Lean 4 follows a structured commit message format derived from the AngularJS convention:

<type>: <subject>

<body>

<footer>

Type prefixes

Type	Meaning
`feat`	New feature
`fix`	Bug fix
`doc`	Documentation only
`style`	Formatting, missing semicolons, etc.
`refactor`	Code restructuring without behavior change
`test`	Adding missing tests
`chore`	Maintenance (CI, tooling, etc.)
`perf`	Performance improvement

Subject rules

Use imperative, present tense: “add” not “added” or “adds”
Do not capitalize the first letter
No trailing period

Body rules

Use imperative, present tense
Explain why the change was made and contrast with previous behavior
Every feat or fix commit must have a changelog-* label and a body starting with "This PR "

Breaking changes: describe the change, justification, and migration notes
Closed issues: Closes #123, #456

Example commit message

fix: add missing decrement for borrowed argument in lean_ctor_get

This PR fixes a reference-counting leak when `lean_ctor_get` is called
with a borrowed argument that is immediately passed to a consuming function.
Previously the caller was expected to manage the RC but the documentation
was silent on this case.

Closes #4242

PR squash policy

All PRs are squash merged. The final commit message is taken directly from the PR title and description. There is no need to clean up individual commits on your branch. Put questions or extra context that should not appear in the commit history as a PR comment, not in the PR description.

Debugging

GDB / LLDB

gdb and lldb can attach to stage1/bin/lean and display C++ stack traces. Lean variables are not yet printable in a human-readable form, but breakpoints and stack traces work:

# Set a breakpoint on the Lean panic handler
gdb build/release/stage1/bin/lean
(gdb) b lean_panic_fn
(gdb) run --server

# With LLDB
lldb build/release/stage1/bin/lean
(lldb) b lean_panic_fn
(lldb) process launch -- --server

Use the debug or sandebug preset when you need full debug symbols:

cmake --preset debug
make -C build/debug -j$(nproc)
gdb build/debug/stage1/bin/lean

Tracing in the elaborator

In CoreM and derived monads, use trace[myClass] "message {expr}" to emit structured traces viewable with:

set_option trace.myClass true

Notable built-in trace classes:

Class	What it traces
`Elab.command`	Command macro expansion and elaboration steps
`Elab.step`	Individual elaboration steps
`Meta.synthInstance`	Type-class synthesis
`Meta.isDefEq`	Definitional equality checking
`interpreter`	Full interpreter execution (debug builds only)

For pure contexts or when the process terminates early, use dbg_trace:

def myFn (x : Nat) : Nat :=
  dbg_trace "myFn called with {x}"
  x + 1

The `rr` reverse debugger

For rare but hard-to-reproduce bugs such as reference-counting errors leading to segfaults, the rr reverse debugger allows you to record a trace and replay it backwards:

rr record build/debug/stage1/bin/lean myfile.lean
rr replay
(rr) reverse-continue

Avoiding downstream rebuilds

When testing changes against a downstream project without wanting to rebuild its entire .olean cache:

# For a single command
LEAN_GITHASH=$(lean --githash) lake +lean4 build

# For a shell session
export LEAN_GITHASH=$(lean --githash)
export ELAN_TOOLCHAIN=lean4

Development

Lean 4 Development Workflow: Editor Setup and Testing

Setting Up Your Editor with elan

Switching toolchains on the fly

VS Code setup

The Bootstrapping Pipeline

The three-stage build

When to update stage0

CCache during development

The `prelude` keyword

Testing

Running the full test suite

Running a specific test

Test suite layout

Testing against Mathlib

Commit Convention

Type prefixes

Subject rules

Body rules

Footer

Example commit message

PR squash policy

Debugging

GDB / LLDB

Tracing in the elaborator

The `rr` reverse debugger

Avoiding downstream rebuilds

Build docs developers (and LLMs) love

Development

Documentation Index

​Setting Up Your Editor with elan

​Switching toolchains on the fly

​VS Code setup

​The Bootstrapping Pipeline

​The three-stage build

​When to update stage0

​CCache during development

​The prelude keyword

​Testing

​Running the full test suite

​Running a specific test

​Test suite layout

​Testing against Mathlib

​Commit Convention

​Type prefixes

​Subject rules

​Body rules

​Footer

​Example commit message

​PR squash policy

​Debugging

​GDB / LLDB

​Tracing in the elaborator

​The rr reverse debugger

​Avoiding downstream rebuilds

Build docs developers (and LLMs) love

Setting Up Your Editor with elan

Switching toolchains on the fly

VS Code setup

The Bootstrapping Pipeline

The three-stage build

When to update stage0

CCache during development

The `prelude` keyword

Testing

Running the full test suite

Running a specific test

Test suite layout

Testing against Mathlib

Commit Convention

Type prefixes

Subject rules

Body rules

Footer

Example commit message

PR squash policy

Debugging

GDB / LLDB

Tracing in the elaborator

The `rr` reverse debugger

Avoiding downstream rebuilds