stage2-build

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:

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),

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:

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).