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

chore: hints about ccache in CLAUDE.md (#12960)

Browse source 
This PR adds instructions for building Lean with ccache in sandboxes.
This commit is contained in:
Joachim Breitner 2026-03-18 11:01:26 +01:00 • committed by GitHub
parent f0b367d7aa
commit 0717cb73d5
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 5 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
.claude/CLAUDE.md
View file

@ -1,7 +1,12 @@
(In the following, use `sysctl -n hw.logicalcpu` instead of `nproc` on macOS)
## Building
To build Lean you should use `make -j$(nproc) -C build/release`.
The build uses `ccache`, and in a sandbox `ccache` may complain about read-only file systems.
Use `CCACHE_READONLY` and `CCACHE_TEMPDIR` instead of disabling ccache completely.
## Running Tests
See `tests/README.md` for full documentation. Quick reference: