Skip to content

Commit

Permalink
chore: add parallelism fallback for macOS on build (#4647)
Browse files Browse the repository at this point in the history
1 less thing to think about.

---------

Co-authored-by: Sebastian Ullrich <[email protected]>
  • Loading branch information
alok and Kha authored Aug 8, 2024
1 parent bcbd729 commit 6dd5023
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions doc/make/index.md
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down

0 comments on commit 6dd5023

Please sign in to comment.