doc: update make docs
This commit is contained in:
Sebastian Ullrich
parent
279746fa6a
commit
274e6bf931
1 changed files with 54 additions and 37 deletions
|
|
@ -12,7 +12,7 @@ Platform-Specific Setup
|
|||
- [Windows (msys2)](msys2.md)
|
||||
- [Windows (Visual Studio)](msvc.md)
|
||||
- [macOS (homebrew)](osx-10.9.md)
|
||||
- Linux/macOS/WSL ([Nix](https://nixos.org/nix/)): Call `nix-shell` in the project root. That's it.
|
||||
- Linux/macOS/WSL via [Nix](https://nixos.org/nix/): Call `nix-shell` in the project root. That's it.
|
||||
|
||||
Generic Build Instructions
|
||||
--------------------------
|
||||
|
|
@ -24,7 +24,7 @@ git clone https://github.com/leanprover/lean4
|
|||
cd lean
|
||||
mkdir -p build/release
|
||||
cd build/release
|
||||
cmake ../../src
|
||||
cmake ../..
|
||||
make
|
||||
```
|
||||
|
||||
|
|
@ -35,14 +35,16 @@ git clone https://github.com/leanprover/lean4
|
|||
cd lean
|
||||
mkdir -p build/debug
|
||||
cd build/debug
|
||||
cmake -D CMAKE_BUILD_TYPE=DEBUG ../../src
|
||||
cmake -D CMAKE_BUILD_TYPE=DEBUG ../..
|
||||
make
|
||||
```
|
||||
|
||||
Add `-jN` for an appropriate `N` to `make` for a parallel build.
|
||||
|
||||
Useful CMake Configuration Settings
|
||||
-----------------------------------
|
||||
|
||||
Pass these along with the `cmake ../../src` command.
|
||||
Pass these along with the `cmake ../..` command.
|
||||
|
||||
* `-D CMAKE_BUILD_TYPE=`\
|
||||
Select the build type. Valid values are `RELEASE` (default), `DEBUG`,
|
||||
|
|
@ -50,7 +52,8 @@ Pass these along with the `cmake ../../src` command.
|
|||
|
||||
* `-D CMAKE_C_COMPILER=`\
|
||||
`-D CMAKE_CXX_COMPILER=`\
|
||||
Select the C++ compiler to use.
|
||||
Select the C/C++ compilers to use. Official Lean releases currently use Clang;
|
||||
see also `.github/workflows/ci.yml` for the CI config.
|
||||
|
||||
* `-D CHECK_OLEAN_VERSION=OFF`\
|
||||
The `.olean` files are tagged with the Lean version they were produced with.
|
||||
|
|
@ -66,41 +69,55 @@ Lean Build Pipeline
|
|||
|
||||
Since version 4, Lean is a partially bootstrapped program: parts of the frontend
|
||||
and compiler are written in Lean itself and thus need to be built before
|
||||
building Lean itself - which is needed to again build those parts. Building the
|
||||
`lean` executable (e.g. via `make bin`) involves roughly the following steps:
|
||||
building Lean itself - which is needed to again build those parts. This cycle is
|
||||
broken by using pre-built C files checked into the repository (which ultimately
|
||||
go back to a point where the Lean compiler was not written in Lean) in place of
|
||||
these Lean inputs and then compiling everything in multiple stages up to a fixed
|
||||
point:
|
||||
|
||||
* The target `stage0` compiles an initial `lean` executable directly from C/C++
|
||||
code versioned in `stage0/` (via a CMake `ExternProject`). The C++ code is a
|
||||
previous version of the code in `src/`, while the C code was extracted from
|
||||
the Lean stdlib of the same commit.
|
||||
* Using this executable, the stdlib contained in `src/Init/` is compiled to
|
||||
`.olean` object files as well as extracted to C in `src/stage1` by the target
|
||||
`make_stdlib`.
|
||||
* The static libraries `leanstdlib` and `leanstatic` are built from the extracted
|
||||
files and the current C++ code in `src/`, respectively.
|
||||
* These libraries are linked into the final `lean` executable.
|
||||
* The `bin` target finally copies all these objects into `bin/`. The initial
|
||||
`lean` executable is called `lean_stage0` there.
|
||||
* stage0: Compiled from C/C++ files in `stage0/src` of a previous version of Lean.
|
||||
This stage should always build since `stage0/` is not changed in the regular
|
||||
workflow.
|
||||
* stage1: Compiled from Lean/C++ files in `src` using the stage0 compiler. This
|
||||
stage is usually sufficient for testing local changes.
|
||||
* stage2: Compiled from Lean/C++ files in `src` using the stage1 compiler. This
|
||||
stage can be used to test changes in stage1 on the stdlib.
|
||||
* stage3: Compiled from Lean/C++ files in `src` using the stage2 compiler. This
|
||||
stage is a sanity check and should usually be identical to stage2. The target
|
||||
`check-stage3` implements this check.
|
||||
|
||||
Development Workflows
|
||||
---------------------
|
||||
Each of these stages has a corresponding subdirectory in the CMake build folder.
|
||||
They can be built by calling `make stageX` in the root build folder, or navigating
|
||||
into the stage build folder and using more specific targets (e.g. `make test`).
|
||||
`make` by itself in the root build folder is short for `make stage1`. Note that since
|
||||
each stage is a separate CMake project, calling `make` inside a stage build folder
|
||||
will never rebuild other stages.
|
||||
|
||||
* The `make_stdlib` target can be used to check the standard library without
|
||||
rebuilding `lean`.
|
||||
* In most cases, the `bin` target can be used to build and test either a Lean or
|
||||
C++ change. The `lean` target can be used to build the same binary without copying
|
||||
it to `bin/`, which can be useful for quickly building a debug version without
|
||||
changing the binary used by the editor. The `LEAN_PATH` variable may need to be set
|
||||
to the location of `src/Init` manually in this case.
|
||||
* Changes in the frontend or compiler do not immediately affect the stdlib because of
|
||||
the staged build until stage0 is updated by making the `update-stage0` target, after
|
||||
which the stdlib can be updated appropriately if necessary. Alternatively, the
|
||||
`bin_lean_stage2` target can be used to build a binary `bin/lean_stage2` from stage1
|
||||
without updating stage0. The build is done in a separate directory (`<build>/stage2`)
|
||||
and has a Makefile dependency on the stage1 binary, which in practice means that
|
||||
*any* change in `src/` leads to a complete rebuild of stage2. Finally, the
|
||||
`check-stage3` target analogously builds a stage3 binary from stage2 and checks that
|
||||
they are bitwise equal (which they should always be given a deterministic build).
|
||||
Development Setup
|
||||
-----------------
|
||||
|
||||
`make test`/`ctest` inside a stage build directory will automatically use the
|
||||
corresponding Lean executables, but for running tests or compiling Lean programs
|
||||
manually, you need to put them into your `PATH` yourself. A simple option for doing
|
||||
that is to register them as custom toolchains in [`elan`](https://github.com/Kha/elan):
|
||||
```
|
||||
# in the Lean rootdir
|
||||
elan toolchain link lean4 build/release/stage1
|
||||
# make `lean` etc. point to the given build in the rootdir and subdirs
|
||||
elan override set lean4
|
||||
```
|
||||
You can also use the `+toolchain` shorthand (e.g. `lean +lean4-debug`) to switch
|
||||
toolchains on the spot.
|
||||
|
||||
Likewise for editor support, `elan` makes it simple to use a stage0 for editing
|
||||
the stdlib while using a different stage for all other files:
|
||||
```
|
||||
elan toolchain link lean4-stage0 build/release/stage0
|
||||
cd src
|
||||
elan override set lean4-stage0
|
||||
```
|
||||
Assuming `lean4-rootdir` is unset, `lean4-mode` will automatically use the
|
||||
correct `lean` executable for the current file.
|
||||
|
||||
Troubleshooting
|
||||
---------------
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue