201 lines
8.5 KiB
Markdown
201 lines
8.5 KiB
Markdown
Requirements
|
|
------------
|
|
|
|
- C++14 compatible compiler
|
|
- [CMake](http://www.cmake.org)
|
|
- [GMP (GNU multiprecision library)](http://gmplib.org/)
|
|
|
|
Platform-Specific Setup
|
|
-----------------------
|
|
|
|
- [Linux (Ubuntu)](ubuntu.md)
|
|
- [Windows (msys2)](msys2.md)
|
|
- [Windows (Visual Studio)](msvc.md)
|
|
- [macOS (homebrew)](osx-10.9.md)
|
|
- Linux/macOS/WSL via [Nix](https://nixos.org/nix/): Call `nix-shell` in the project root. That's it.
|
|
|
|
Generic Build Instructions
|
|
--------------------------
|
|
|
|
Setting up a basic release build:
|
|
|
|
```bash
|
|
git clone https://github.com/leanprover/lean4
|
|
cd lean
|
|
mkdir -p build/release
|
|
cd build/release
|
|
cmake ../..
|
|
make
|
|
```
|
|
|
|
Setting up a basic debug build:
|
|
|
|
```bash
|
|
git clone https://github.com/leanprover/lean4
|
|
cd lean
|
|
mkdir -p build/debug
|
|
cd build/debug
|
|
cmake -D CMAKE_BUILD_TYPE=DEBUG ../..
|
|
make
|
|
```
|
|
|
|
This will compile the Lean library and binary into the `stage0.5` subfolder; see
|
|
below for details. Add `-jN` for an appropriate `N` to `make` for a parallel
|
|
build.
|
|
|
|
Useful CMake Configuration Settings
|
|
-----------------------------------
|
|
|
|
Pass these along with the `cmake ../..` command.
|
|
|
|
* `-D CMAKE_BUILD_TYPE=`\
|
|
Select the build type. Valid values are `RELEASE` (default), `DEBUG`,
|
|
`RELWITHDEBINFO`, and `MINSIZEREL`.
|
|
|
|
* `-D CMAKE_C_COMPILER=`\
|
|
`-D CMAKE_CXX_COMPILER=`\
|
|
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.
|
|
This means that by default, the core library has to be recompiled after e.g.
|
|
every `git commit`. Use this option to avoid the version check. The `.olean`
|
|
files can be removed manually by invoking `make clean-olean`.
|
|
|
|
Lean will automatically use [CCache](https://ccache.dev/) if available to avoid
|
|
redundant builds, especially after stage 0 has been updated (see below).
|
|
|
|
Lean Build Pipeline
|
|
-------------------
|
|
|
|
Since version 4, Lean is a partially bootstrapped program: most 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. 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 build directory is organized in these stages:
|
|
|
|
```bash
|
|
stage0/
|
|
bin/
|
|
lean # the Lean compiler & server
|
|
leanc # a wrapper around a C compiler supplying search paths etc
|
|
leanmake # a wrapper around `make` supplying the Makefile below
|
|
lib/
|
|
lean/**/*.olean # the Lean library (incl. the compiler) compiled by `lean` above
|
|
temp/**/*.{c,o} # the library extracted to C and compiled by `leanc`
|
|
libInit.a # a static library of the Lean library
|
|
libleancpp.a # a static library of the C++ sources of Lean
|
|
include/
|
|
config.h # config variables used to build `lean` such as use allocator
|
|
runtime/lean.h # runtime headers, used by extracted C code, uses `config.h`
|
|
share/lean/
|
|
Makefile # used by `leanmake`
|
|
stage1/...
|
|
stage2/...
|
|
stage3/...
|
|
```
|
|
|
|
The build for each stage starts by assembling `bin/lean` from the `libInit.a` of
|
|
the preceding stage and `libleancpp.a` built from `src/`; in the case of stage 0,
|
|
which doesn't have a preceding stage, both libraries are instead assembled from
|
|
`stage0/src`, which contains the C++ and extracted C code of a previous commit of
|
|
Lean. This Lean binary is then used to compile the Lean library into .olean files
|
|
and ultimately a new `libInit.a`, which is then used by the next stage.
|
|
|
|
Each stage can be built by calling `make stageN` in the root build folder. It is
|
|
usually not necessary to compile all stages in order to test a change. Stage 3 in
|
|
fact should usually be identical to stage 2 and only exists as a sanity check,
|
|
which can be done via `make check-stage3`. Building stage 2 should only be
|
|
necessary for testing how changes in the compiler influence compilation of the
|
|
compiler itself, e.g. checking if an optimization speeds up (or breaks) the
|
|
compiler. Stage 1 is sufficient for testing changes on the library and test
|
|
programs. In fact, if the stage 0 library and the stage 1 are compatible (use the
|
|
same Lean ABI, so to speak), we can avoid even rebuilding the stage 1 library
|
|
using a special stage "0.5" that combines the stage 1 compiler with the stage 0
|
|
library. Most changes do not break this ABI, so running `make` by itself in the
|
|
root build folder will default to `make stage0.5`. In summary, doing a standard
|
|
build via `make` involves these steps:
|
|
|
|
1. compile the `stage0/src` archived sources into `stage0/bin/lean`
|
|
1. use it to compile the library (*including* your changes) into `stage0/lib`
|
|
1. link that and the *current* C++ code from `src/` into `stage1/bin/lean`
|
|
1. copy ("uplift") the Lean library from `stage0/lib` into `stage1/lib`
|
|
|
|
You now have a Lean binary and library that include your changes, though their
|
|
own compilation was not influenced by them, that you can use to test your changes
|
|
on test programs whose compilation *will* be influenced by the changes.
|
|
|
|
Finally, when we want to use new language features in the library, we need to
|
|
update the stage 0 compiler, which can be done via `make -C stageN update-stage0`.
|
|
Note: you cannot do this for stage 0.5 because the extracted C files are not
|
|
copied over from stage 0 to that stage, so just use stage 0 instead.
|
|
`make update-stage0` without `-C` defaults to stage0 for this reason. If updating
|
|
stage 0 from stage 0 sounds wrong to you, just remember that the stage 0 build
|
|
directory contains the *output* of the stage 0 compiler!
|
|
|
|
Development Setup
|
|
-----------------
|
|
|
|
After building a stage, you can invoke `make -C stageN test` (or, even better,
|
|
`make -C stageN ARGS=-j` to make `ctest` parallel) to run the Lean test suite.
|
|
`make test` without `-C` defaults to stage 0.5. While the Lean tests
|
|
will automatically use that stage's corresponding Lean executables, 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 use
|
|
[`elan`](https://github.com/Kha/elan), see the next section.
|
|
|
|
The only currently supported editor is Emacs, see `lean4-mode/README.md` for
|
|
basic setup. You can set `lean4-rootdir` manually to tell it what stage to use:
|
|
```
|
|
# while editing the Lean library
|
|
M-x set-variable lean4-rootdir RET ".../build/release/stage0" RET
|
|
# while testing, using a Lean that includes your changes
|
|
M-x set-variable lean4-rootdir RET ".../build/release/stage0.5" RET
|
|
```
|
|
but `elan` again makes it simple to do that automatically, see below.
|
|
|
|
Dev setup using elan
|
|
--------------------
|
|
|
|
You can use [`elan`](https://github.com/Kha/elan) to easily switch between
|
|
stages and build configurations based on the current directory, both for the
|
|
`lean/leanc/leanmake` binaries in your shell's PATH and inside Emacs.
|
|
|
|
If you haven't already installed elan, you can do so, without installing a
|
|
default version of Lean, using
|
|
```bash
|
|
curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none
|
|
```
|
|
You can use `elan toolchain link` to give a specific stage build directory a
|
|
reference name, then use `elan override set` to associate such a name to the
|
|
current directory. We usually want to use `stage0` for editing files in `src`
|
|
and `stage0.5` for everything else (e.g. tests).
|
|
```
|
|
# in the Lean rootdir
|
|
elan toolchain link lean4 build/release/stage0.5
|
|
elan toolchain link lean4-stage0 build/release/stage0
|
|
# make `lean` etc. point to stage0.5 in the rootdir and subdirs
|
|
elan override set lean4
|
|
cd src
|
|
# make `lean` etc. point to stage0 anywhere inside `src`
|
|
elan override set lean4-stage0
|
|
```
|
|
You can also use the `+toolchain` shorthand (e.g. `lean +lean4-debug`) to switch
|
|
toolchains on the spot. `lean4-mode` will automatically use the `lean` executable
|
|
associated with the directory of the current file as long as `lean4-rootdir` is
|
|
unset and `~/.elan/bin` is in your `exec-path`. Where Emacs sources the
|
|
`exec-path` from can be a bit unclear depending on your configuration, so
|
|
alternatively you can also set `lean4-rootdir` to `"~/.elan"` explicitly.
|
|
|
|
You might find that debugging through elan, e.g. via `gdb lean`, disables some
|
|
things like symbol autocompletion because at first only the elan proxy binary
|
|
is loaded. You can instead pass the explicit path to `bin/lean` in your build
|
|
folder to gdb, or use `gdb $(elan which lean)`.
|
|
|
|
Troubleshooting
|
|
---------------
|
|
|
|
* Call `make` with an additional `VERBOSE=1` argument to print executed commands.
|