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

chore: add parallelism fallback for macOS on build (#4647)

Browse source 
1 less thing to think about.

---------

Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
This commit is contained in:
Alok Singh 2024-08-08 07:26:06 -07:00 • committed by GitHub
parent bcbd7299e9
commit 6dd502321f
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
doc/make/index.md
View file

@ -27,9 +27,9 @@ Setting up a basic parallelized release build:
git clone https://github.com/leanprover/lean4
cd lean4
cmake --preset release
make -C build/release -j$(nproc) # see below for macOS
make -C build/release -j$(nproc || sysctl -n hw.logicalcpu)
```
You can replace `$(nproc)`, which is not available on macOS and some alternative shells, with the desired parallelism amount.
You can replace `$(nproc || sysctl -n hw.logicalcpu)` with the desired parallelism amount.
The above commands will compile the Lean library and binaries into the
`stage1` subfolder; see below for details.