max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: CLAUDE.md: restrict build parallelism (#12624)

Browse source
This commit is contained in:
Sebastian Ullrich 2026-02-22 15:35:05 +01:00 • committed by GitHub
parent 2e7fe7e79d
commit 5115229be2
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 7 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
.claude/CLAUDE.md
View file

@ -1,4 +1,6 @@
To build Lean you should use `make -j -C build/release`.
(In the following, use `sysctl -n hw.logicalcpu` instead of `nproc` on macOS)
To build Lean you should use `make -j$(nproc) -C build/release`.
## Running Tests
@ -6,13 +8,13 @@ See `doc/dev/testing.md` for full documentation. Quick reference:
```bash
# Full test suite (use after builds to verify correctness)
make -j -C build/release test ARGS="-j$(nproc)"
make -j$(nproc) -C build/release test ARGS="-j$(nproc)"
# Specific test by name (supports regex via ctest -R)
make -j -C build/release test ARGS='-R grind_ematch --output-on-failure'
make -j$(nproc) -C build/release test ARGS='-R grind_ematch --output-on-failure'
# Rerun only previously failed tests
make -j -C build/release test ARGS='--rerun-failed --output-on-failure'
make -j$(nproc) -C build/release test ARGS='--rerun-failed --output-on-failure'
# Single test from tests/lean/run/ (quick check during development)
cd tests/lean/run && ./test_single.sh example_test.lean
@ -41,7 +43,7 @@ All new tests should go in `tests/lean/run/`. These tests don't have expected ou
## Build System Safety
**NEVER manually delete build directories** (build/, stage0/, stage1/, etc.) even when builds fail.
- ONLY use the project's documented build command: `make -j -C build/release`
- ONLY use the project's documented build command: `make -j$(nproc) -C build/release`
- If a build is broken, ask the user before attempting any manual cleanup
## LSP and IDE Diagnostics