From f64a3431835ca7558ca61c893a67f468c74518e2 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 14 May 2020 13:48:36 +0200 Subject: [PATCH] doc: describe new bootstrap setup --- doc/make/coverage.md | 28 ---------- doc/make/index.md | 108 ++++++++++++++++++++++++++------------- doc/make/split-stack.md | 72 -------------------------- doc/make/ubuntu-16.04.md | 6 +++ lean4-mode/README.md | 3 +- 5 files changed, 80 insertions(+), 137 deletions(-) delete mode 100644 doc/make/coverage.md delete mode 100644 doc/make/split-stack.md create mode 100644 doc/make/ubuntu-16.04.md diff --git a/doc/make/coverage.md b/doc/make/coverage.md deleted file mode 100644 index 5f35817284..0000000000 --- a/doc/make/coverage.md +++ /dev/null @@ -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 diff --git a/doc/make/index.md b/doc/make/index.md index cde2e16411..6b0da3b4f2 100644 --- a/doc/make/index.md +++ b/doc/make/index.md @@ -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) diff --git a/doc/make/split-stack.md b/doc/make/split-stack.md deleted file mode 100644 index 0cb2a1b2e0..0000000000 --- a/doc/make/split-stack.md +++ /dev/null @@ -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](). - -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`. diff --git a/doc/make/ubuntu-16.04.md b/doc/make/ubuntu-16.04.md new file mode 100644 index 0000000000..b166e32447 --- /dev/null +++ b/doc/make/ubuntu-16.04.md @@ -0,0 +1,6 @@ +Installing Lean on Ubuntu 16.04 +------------------------------- + +### Basic packages + + sudo apt-get install git libgmp-dev cmake ccache diff --git a/lean4-mode/README.md b/lean4-mode/README.md index 84542a1c0e..67e795184c 100644 --- a/lean4-mode/README.md +++ b/lean4-mode/README.md @@ -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) ```