stage2-build
Build and run tests against the stage2 Lean compiler. Use when asked to build, rebuild, or test against stage2.
Source facts
- Repository
- leanprover/lean4
- Last source activity
- June 10, 2026 at 11:48
- Detected SKILL.md language
- English
- Stars
- 9,735
- Forks
- 1,076
Install options
The review-first prompt is selected by default. You can switch to a direct command or download a local copy.
Review the source files
Read SKILL.md and any companion files shown by SkillsMP before deciding whether to install.
Showing SKILL.md
SKILL.md
Source instructions · Read-only preview- name
- stage2-build
- description
- Build and run tests against the stage2 Lean compiler. Use when asked to build, rebuild, or test against stage2.
- allowed-tools
- Bash, Read
# Testing Stage 2
Building stage2 is expensive, so confirm with the user before starting a stage2 build.
Build it as follows:
```bash
make -C build/release stage2 -j$(nproc)
```
Stage 2 is *not* automatically invalidated by changes to `src/`, which allows for faster iteration
when fixing a specific file in the stage 2 build. But to invalidate any files that already passed the
stage 2 build (as well as for final validation),
```bash
make -C build/release/stage2 clean-stdlib
```
must be run manually before building.
To rebuild individual stage 2 modules without a full `make stage2`, use Lake directly:
```bash
cd build/release/stage2 && lake build Init.Prelude
```
To run tests in stage2, replace `-C build/release` with `-C build/release/stage2` in the usual test
commands (see the project `.claude/CLAUDE.md` "Running Tests" section).
View on GitHub