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

doc: restructure make/index.md

Browse source 
debug builds are not very interesting currently given the state of
debugging Lean code
This commit is contained in:
Sebastian Ullrich 2021-10-08 19:36:25 +02:00 • committed by Leonardo de Moura
parent 6296151034
commit 74b813fbcd
1 changed files with 4 additions and 19 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

23
doc/make/index.md
View file

@ -31,30 +31,15 @@ cmake ../..
make
```
Note: that if you have a CPU with lots of cores you will get a faster
build if you specify the number of parallel jobs using the `-j n`
option on make.
The above commands will compile the Lean library and binaries into the
`stage1` subfolder; see below for details. Add `-j N` for an
appropriate `N` to `make` for a parallel build.
For example, on an AMD Ryzen 9 `make` takes 00:04:55, whereas `make -j 10`
takes 00:01:38. Your results may vary depending on the speed of your hard
drive.
Setting up a basic debug build:
```bash
git clone https://github.com/leanprover/lean4
cd lean4
mkdir -p build/debug
cd build/debug
cmake -D CMAKE_BUILD_TYPE=DEBUG ../..
make
```
This will compile the Lean library and binary into the `stage1` subfolder; see
below for details. Add `-jN` for an appropriate `N` to `make` for a parallel
build.
To install the build see [Dev setup using
To install the build, see [Dev setup using
elan](../dev/index.md#dev-setup-using-elan).