stage2-build
Build and run tests against the stage2 Lean compiler. Use when asked to build, rebuild, or test against stage2.
Datos de origen
- Repositorio
- leanprover/lean4
- Última actividad en el origen
- 10 de junio de 2026 a las 11:48
- Idioma detectado de SKILL.md
- inglés
- Estrellas
- 9551
- Forks
- 1044
Opciones de instalación
De forma predeterminada está seleccionado el prompt que primero revisa el origen. Puedes cambiar a un comando directo o descargar una copia local.
Revisa los archivos de origen
Lee SKILL.md y los archivos complementarios que muestra SkillsMP antes de decidir si quieres instalarlo.
Mostrando SKILL.md
SKILL.md
Instrucciones de origen · Vista previa de solo lectura- 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).
Ver en GitHub