sdgoij/lean4
1
0
Fork 0
mirror of https://github.com/leanprover/lean4.git synced 2026-03-17 10:24:07 +00:00
Code Issues Packages Projects Releases Wiki Activity

chore: CLAUDE.md: stage 2 build instructions (#12929)

Browse Source
This commit is contained in:
Sebastian Ullrich
2026-03-16 10:47:14 +01:00
committed by GitHub
parent c9ceba1784
commit ddd5c213c6
1 changed files with 14 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

14
.claude/CLAUDE.md
View File

@@ -23,6 +23,20 @@ make -C build/release -j "$(nproc)" test ARGS='--rerun-failed'
cd tests/foo/bar && ./run_test example_test.lean
```
## Testing stage 2
When requested to test stage 2, 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 for invalidating 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.
## New features
When asked to implement new features: