Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

chore: add parallelism fallback for macOS on build #4647

Merged
merged 2 commits into from
Aug 8, 2024
Merged

chore: add parallelism fallback for macOS on build #4647

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
361bb45
chore: add parallelism fallback for macOS on build
alok Jul 3, 2024
7da4e1c
Update doc/make/index.md
Kha Aug 8, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions doc/make/index.md
View file
Open in desktop
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
Loading