mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
doc: describe new bootstrap setup
This commit is contained in:
Sebastian Ullrich
@@ -1,28 +0,0 @@
|
||||
Instructions for Testing and Measuring Code Coverage
|
||||
====================================================
|
||||
|
||||
To measure code coverage, compile TESTCOV build using g++:
|
||||
|
||||
mkdir -p build/testcov
|
||||
cd build/testcov
|
||||
cmake -DCMAKE_BUILD_TYPE=Debug -DTESTCOV=ON -DCMAKE_CXX_COMPILER=g++-4.8 -G Ninja ../../src
|
||||
|
||||
and run:
|
||||
|
||||
ninja cov
|
||||
|
||||
It will build the project, run testcases, and compute code-coverage.
|
||||
In the end, you have ``build/testcov/coverage`` directory containing
|
||||
a code-coverage report in HTML format.
|
||||
|
||||
Make sure that the version of ``gcov`` matches with the one of
|
||||
``g++``. Also try to use the latest ``lcov`` (currently lcov-1.10)
|
||||
if you have a problem with the existing one:
|
||||
|
||||
wget http://downloads.sourceforge.net/ltp/lcov-1.10.tar.gz;
|
||||
tar xvfz lcov-1.10.tar.gz;
|
||||
cp -v lcov-1.10/bin/{lcov,genpng,gendesc,genhtml,geninfo} /usr/bin/;
|
||||
rm -rf lcov-1.10.tar.gz lcov-1.10;
|
||||
|
||||
[gcov]: http://gcc.gnu.org/onlinedocs/gcc/Gcov.html
|
||||
[lcov]: http://ltp.sourceforge.net/coverage/lcov.php
|
||||
@@ -39,7 +39,9 @@ cmake -D CMAKE_BUILD_TYPE=DEBUG ../..
|
||||
make
|
||||
```
|
||||
|
||||
Add `-jN` for an appropriate `N` to `make` for a parallel build.
|
||||
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
|
||||
-----------------------------------
|
||||
@@ -67,65 +69,101 @@ redundant builds, especially after stage 0 has been updated (see below).
|
||||
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
|
||||
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:
|
||||
point. The build directory is organized in these stages:
|
||||
|
||||
* 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.
|
||||
```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/...
|
||||
```
|
||||
|
||||
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 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. 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
|
||||
-----------------
|
||||
|
||||
`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):
|
||||
After building a stage, you can invoke `ctest` (or, even better, `ctest -j`)
|
||||
inside the stage build directory to run the Lean test suite. 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 register them as custom toolchains
|
||||
in [`elan`](https://github.com/Kha/elan):
|
||||
```
|
||||
# in the Lean rootdir
|
||||
elan toolchain link lean4 build/release/stage1
|
||||
elan toolchain link lean4 build/release/stage0.5
|
||||
# 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:
|
||||
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,
|
||||
but `elan` again makes it simple to do that automatically, e.g. using stage 0
|
||||
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
|
||||
---------------
|
||||
|
||||
* Call `make` with an additional `VERBOSE=1` argument to print executed commands.
|
||||
|
||||
Further Information
|
||||
-------------------
|
||||
|
||||
- [Measuring Code Coverage](coverage.md)
|
||||
- [Compiling Lean with Split Stacks](split-stack.md)
|
||||
|
||||
@@ -1,72 +0,0 @@
|
||||
Compiling Lean with Split Stacks
|
||||
================================
|
||||
|
||||
[Split stacks](http://gcc.gnu.org/wiki/SplitStacks) is a relatively
|
||||
new feature in gcc. It allows the stack to grown automatically as
|
||||
needed. There is a small performance penalty since the program stack
|
||||
is stored in the heap. However, we can have multiple threads, each starting
|
||||
with a small stack, and have the stack grow and shrink as required by
|
||||
the program.
|
||||
|
||||
In principle, it is possible to build a program that uses split-stacks
|
||||
with libraries that do not. However, it did not work in our experiments.
|
||||
To be able to compile Lean with split-stacks, we also have to compile
|
||||
GMP using split-stacks.
|
||||
|
||||
We also had to use the [gold linker](<http://en.wikipedia.org/wiki/Gold_(linker)>).
|
||||
|
||||
Gold linker
|
||||
-----------
|
||||
|
||||
The gold linker is called `ld.gold` (in our test system). On Ubuntu, you
|
||||
can install it by executing
|
||||
|
||||
sudo apt-get install binutils-gold
|
||||
|
||||
Before we compiled GMP and Lean, we created an alias
|
||||
|
||||
alias ld=ld.gold
|
||||
|
||||
If everything is working correctly, when we execute `ld --version`, we should
|
||||
get an output like the following one:
|
||||
|
||||
GNU gold (GNU Binutils for Ubuntu 2.22) 1.11
|
||||
Copyright 2011 Free Software Foundation, Inc.
|
||||
...
|
||||
|
||||
Compiling GMP using split-stacks
|
||||
--------------------------------
|
||||
|
||||
Download GMP from [https://gmplib.org](https://gmplib.org/); uncompress the gmp tar-ball at `$HOME/tools`; and configure it using
|
||||
|
||||
./configure CFLAGS=-fsplit-stack --prefix=$HOME/tools/split-stack --enable-static
|
||||
|
||||
Then, build and install using
|
||||
|
||||
make
|
||||
make install
|
||||
|
||||
We should have the file `libgmp.a` at `$HOME/tools/split-stack/lib`.
|
||||
|
||||
Compiling Lean using split-stacks
|
||||
--------------------------------
|
||||
|
||||
Go to the Lean directory, and create the folder `build/release`
|
||||
|
||||
mkdir build/release
|
||||
|
||||
Configure Lean using
|
||||
|
||||
cmake -D CMAKE_BUILD_TYPE=Release -D CMAKE_CXX_COMPILER=g++ -D TCMALLOC=OFF -D GMP_INCLUDE_DIR=$HOME/tools/split-stack/include -D GMP_LIBRARIES=$HOME/tools/split-stack/lib/libgmp.a ../../src
|
||||
|
||||
Remark: if you have ninja build tool installed in your system, you can also provide `-G Ninja`
|
||||
|
||||
Then, build using
|
||||
|
||||
make
|
||||
|
||||
and, test it
|
||||
|
||||
yes "C" | ctest
|
||||
|
||||
The Lean executable will be located at `build/release/shell/lean`.
|
||||
6
doc/make/ubuntu-16.04.md
Normal file
6
doc/make/ubuntu-16.04.md
Normal file
@@ -0,0 +1,6 @@
|
||||
Installing Lean on Ubuntu 16.04
|
||||
-------------------------------
|
||||
|
||||
### Basic packages
|
||||
|
||||
sudo apt-get install git libgmp-dev cmake ccache
|
||||
@@ -4,7 +4,7 @@ Installation
|
||||
To use `lean4-mode` in Emacs, add the following to your `init.el`:
|
||||
```
|
||||
;; You need to modify the following line
|
||||
(setq lean4-rootdir "/path/to/lean4-checkout")
|
||||
(setq load-path (cons (concat lean4-rootdir "/path/to/lean4-mode") load-path))
|
||||
|
||||
(setq lean4-mode-required-packages '(dash dash-functional f flycheck s))
|
||||
|
||||
@@ -19,7 +19,6 @@ To use `lean4-mode` in Emacs, add the following to your `init.el`:
|
||||
(setq need-to-refresh nil))
|
||||
(package-install p))))
|
||||
|
||||
(setq load-path (cons (concat lean4-rootdir "/lean4-mode") load-path))
|
||||
(require 'lean4-mode)
|
||||
```
|
||||
|
||||
|
||||
Reference in New Issue
Block a user