doc: refine development manual
This commit is contained in:
Sebastian Ullrich
parent
18707692a8
commit
d2c626e158
9 changed files with 66 additions and 249 deletions
|
|
@ -60,17 +60,15 @@
|
|||
# Development
|
||||
|
||||
- [Development Guide](./dev/index.md)
|
||||
- [Bootstrapping](./dev/bootstrap.md)
|
||||
- [Commit Convention](./dev/commit_convention.md)
|
||||
- [Building Lean](./make/index.md)
|
||||
- [Ubuntu Setup](./make/ubuntu.md)
|
||||
- [macOS Setup](./make/osx-10.9.md)
|
||||
- [Windows MSYS2 Setup](./make/msys2.md)
|
||||
- [Windows with WSL](./make/wsl.md)
|
||||
- [Nix Setup (*Experimental*)](./make/nix.md)
|
||||
- [Foreign Function Interface](./dev/ffi.md)
|
||||
- [Unit Testing](./dev/testing.md)
|
||||
- [Building This Manual](./dev/mdbook.md)
|
||||
- [Fixing Tests](./dev/fixing_tests.md)
|
||||
- [Bootstrapping](./dev/bootstrap.md)
|
||||
- [Testing](./dev/testing.md)
|
||||
- [Debugging](./dev/debugging.md)
|
||||
<!-- - [C++ Coding Style](./dev/cpp_coding_style.md) -->
|
||||
- [Commit Convention](./dev/commit_convention.md)
|
||||
- [Building This Manual](./dev/mdbook.md)
|
||||
- [Foreign Function Interface](./dev/ffi.md)
|
||||
|
|
|
|||
|
|
@ -15,17 +15,18 @@ stage0/
|
|||
bin/lean
|
||||
stage1/
|
||||
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`
|
||||
config.h # config variables used to build `lean` such as used allocator
|
||||
runtime/lean.h # runtime header, used by extracted C code, uses `config.h`
|
||||
share/lean/
|
||||
Makefile # used by `leanmake`
|
||||
lean.mk # used by `leanmake`
|
||||
lib/
|
||||
lean/**/*.olean # the Lean library (incl. the compiler) compiled by the previous stage's `lean`
|
||||
temp/**/*.{c,o} # the library extracted to C and compiled by `leanc`
|
||||
libInit.a libStd.a libLean.a # static libraries of the Lean library
|
||||
libleancpp.a # a static library of the C++ sources of Lean
|
||||
libleanshared.so # a dynamic library including the static libraries above
|
||||
bin/
|
||||
lean # the Lean compiler & server linked together from the above libraries
|
||||
lean # the Lean compiler & server, a small executable that calls directly into libleanshared.so
|
||||
leanc # a wrapper around a C compiler supplying search paths etc
|
||||
leanmake # a wrapper around `make` supplying the Makefile above
|
||||
stage2/...
|
||||
|
|
@ -54,7 +55,7 @@ We are not aware of any "meta-meta" parts that influence more than two stages of
|
|||
compilation, so stage 3 should always be identical to stage 2 and only exists as
|
||||
a sanity check.
|
||||
|
||||
In summary, doing a standard build via `make` involves these steps:
|
||||
In summary, doing a standard build via `make` internally involves these steps:
|
||||
|
||||
1. compile the `stage0/src` archived sources into `stage0/bin/lean`
|
||||
1. use it to compile the current library (*including* your changes) into `stage1/lib`
|
||||
|
|
|
|||
|
|
@ -1,155 +0,0 @@
|
|||
[google-style]: https://google.github.io/styleguide/cppguide.html
|
||||
[cpplint]: /src/cmake/Modules/cpplint.py
|
||||
|
||||
# Coding Style
|
||||
|
||||
The Lean project is moving away from using any C++ as more and more of
|
||||
the compiler is being bootstrapped in Lean itself. But the remaining
|
||||
C++ codebase is using modified version of [Google's C++ Style
|
||||
Guide][google-style].
|
||||
|
||||
## [C++11](http://en.wikipedia.org/wiki/C%2B%2B11) features
|
||||
|
||||
Lean makes extensive use of new features in the C++ 11 standard.
|
||||
Developers must be familiar with the standard to be able to understand
|
||||
the code. Here are some of the features that are extensively used.
|
||||
|
||||
- Type inference (aka `auto` keyword).
|
||||
- Initializer lists.
|
||||
- Lambda functions and expressions.
|
||||
- `nullptr` constant.
|
||||
- Strongly typed enumerations.
|
||||
- Right angle brackets with no space is now allowed in C++ 11.
|
||||
- Thread local storage.
|
||||
- Threading facilities.
|
||||
- Tuple types.
|
||||
- Smart pointers.
|
||||
- When using ``std::list`` make sure to include the `std::`
|
||||
qualifier so you do not accidentally use the ``lean::list`` type.
|
||||
- When using ``std::copy`` make sure to include the `std::`
|
||||
qualifier so you do not accidentally use the ``lean::copy`` type.
|
||||
- Small and focused functions are preferred: foo(). Try not to
|
||||
exceed 500 lines in a function, except in tests.
|
||||
- Do **not** use the `#ifndef-#define-#endif` idiom for header files.
|
||||
Instead use `#pragma once`.
|
||||
- Write `type const & v` instead of `const type & v`.
|
||||
- Use `const` extensively.
|
||||
- Use the macro `lean_assert` for assertions. The macro `lean_assert`
|
||||
is extensively used when writing unit tests.
|
||||
|
||||
## Naming
|
||||
|
||||
- Class, method, and function names are lower case
|
||||
Use `_` for composite names. Example: `type_checker`.
|
||||
- Class/struct fields should start with the prefix `m_`.
|
||||
|
||||
Example:
|
||||
```c++
|
||||
class point {
|
||||
int m_x;
|
||||
int m_y;
|
||||
public:
|
||||
...
|
||||
};
|
||||
```
|
||||
|
||||
## Namespaces
|
||||
|
||||
All code is in the `lean` namespace. Each frontend is stored in a
|
||||
separate nested namespace. For example, the SMT 2.0 frontend is stored
|
||||
in the `lean::smt` namespace.
|
||||
|
||||
Exception: some debugging functions are stored outside of the `lean`
|
||||
namespace. These functions are called `print` and are meant to be used
|
||||
when debugging Lean using `gdb`.
|
||||
|
||||
Do not use `using namespace` in a header file.
|
||||
|
||||
## Templates
|
||||
|
||||
Organize template source code using the approach described at http://www.codeproject.com/Articles/3515/How-To-Organize-Template-Source-Code
|
||||
|
||||
## Idioms
|
||||
|
||||
Use some popular C++ idioms:
|
||||
|
||||
- [Pimpl](http://c2.com/cgi/wiki?PimplIdiom)
|
||||
- [RAII](http://en.wikipedia.org/wiki/Resource_Acquisition_Is_Initialization) Resource Acquisition Is Initialization
|
||||
|
||||
## Formatting
|
||||
|
||||
* Use 4 spaces for indentation.
|
||||
|
||||
* `if-then-else` curly brackets not always required. The following
|
||||
forms are acceptable:
|
||||
|
||||
```c++
|
||||
if (cond) {
|
||||
...
|
||||
} else {
|
||||
...
|
||||
}
|
||||
```
|
||||
and
|
||||
|
||||
```c++
|
||||
if (cond)
|
||||
statement1;
|
||||
else
|
||||
statement2;
|
||||
```
|
||||
|
||||
In *exceptional cases*, we also use
|
||||
|
||||
```c++
|
||||
if (cond) statement;
|
||||
```
|
||||
|
||||
and
|
||||
|
||||
```c++
|
||||
if (cond) statement1; else stament2;
|
||||
```
|
||||
* `if-then-else-if-else`
|
||||
|
||||
The following forms are acceptable:
|
||||
|
||||
```c++
|
||||
if (cond) {
|
||||
...
|
||||
} else if (cond) {
|
||||
...
|
||||
} else {
|
||||
...
|
||||
}
|
||||
```c++
|
||||
and
|
||||
|
||||
```c++
|
||||
if (cond)
|
||||
statement1;
|
||||
else if (cond)
|
||||
statement2;
|
||||
else
|
||||
statement3;
|
||||
```
|
||||
|
||||
* Format code using extra spaces to make code more readable. For example:
|
||||
|
||||
```c++
|
||||
environment const & m_env;
|
||||
cache m_cache;
|
||||
normalizer m_normalizer;
|
||||
volatile bool m_interrupted;
|
||||
```
|
||||
instead of:
|
||||
|
||||
```c++
|
||||
environment const & m_env;
|
||||
cache m_cache;
|
||||
normalizer m_normalizer;
|
||||
volatile bool m_interrupted;
|
||||
```
|
||||
|
||||
* Spaces in expressions. Write `a == b` instead of `a==b`. Similarly,
|
||||
we write `x < y + 1` instead of `x<y+1`.
|
||||
|
|
@ -1,39 +0,0 @@
|
|||
Fixing Tests
|
||||
============
|
||||
|
||||
The test suite contains some tests that compare the produced output
|
||||
with the expected output. For example, the directory `tests/lean`
|
||||
contains files such as [`bad_class.lean`](../tests/lean/bad_class.lean) and
|
||||
[`bad_class.lean.expected.out`](../tests/lean/bad_class.lean.expected.out).
|
||||
The later contains the expected output for the test file `bad_class.lean`.
|
||||
|
||||
When the Lean source code or the standard library are modified, some of these
|
||||
tests break because the produced output is slightly different, and we have
|
||||
to reflect the changes in the `.lean.expected.out` files.
|
||||
We should not blindly copy the new produced output since we may accidentally
|
||||
miss a bug introduced by recent changes.
|
||||
The test suite contains commands that allow us to see what changed in a convenient way.
|
||||
First, we must install [meld](http://meldmerge.org/). On Ubuntu, we can do it by simply executing
|
||||
|
||||
```
|
||||
sudo apt-get install meld
|
||||
```
|
||||
|
||||
Now, suppose `bad_class.lean` test is broken. We can see the problem by going to `test/lean` directory and
|
||||
executing
|
||||
|
||||
```
|
||||
./test_single.sh -i bad_class.lean
|
||||
```
|
||||
|
||||
When the `-i` option is provided, `meld` is automatically invoked
|
||||
whenever there is discrepancy between the produced and expected
|
||||
outputs. `meld` can also be used to repair the problems.
|
||||
|
||||
In Emacs, we can also execute `M-x lean4-diff-test-file` to check/diff the file of the current buffer.
|
||||
To mass-copy all `.produced.out` files to the respective `.expected.out` file, use `tests/lean/copy-produced`.
|
||||
When using the Nix setup, add `--keep-failed` to the `nix build` call and then call
|
||||
```sh
|
||||
tests/lean/copy-produced <build-dir>/source/tests/lean
|
||||
```
|
||||
instead where `<build-dir>` is the path printed out by `nix build`.
|
||||
|
|
@ -1,48 +1,30 @@
|
|||
# Development Workflow
|
||||
- [Commit Convention](./commit_convention.md)
|
||||
- [Building Lean](../make/index.md)
|
||||
- [Ubuntu Setup](../make/ubuntu.md)
|
||||
- [macOS Setup](../make/osx-10.9.md)
|
||||
- [Windows MSYS2 Setup](../make/msys2.md)
|
||||
- [Windows with WSL](../make/wsl.md)
|
||||
- [Nix Setup (*Experimental*)](../make/nix.md)
|
||||
- [Unit Testing](./testing.md)
|
||||
- [Building This Manual](./mdbook.md)
|
||||
- [Fixing Tests](./fixing_tests.md)
|
||||
- [Debugging](./debugging.md)
|
||||
- [C++ Coding Style](./dev/cpp_coding_style.md)
|
||||
|
||||
You will notice there is a `stage0` folder. This is for bootstrapping
|
||||
the compiler development. Generally you do not change any code in
|
||||
`stage0` manually. It is important that you read [bootstrapping
|
||||
pipeline](bootstrap.md) so you understand how this works.
|
||||
If you want to make changes to Lean itself, start by [building Lean](../make/index.html) from a clean checkout to make sure that everything is set up correctly.
|
||||
After that, read on below to find out how to set up your editor for changing the Lean source code, followed by further sections of the development manual where applicable such as on the [test suite](testing.md) and [commit convention](commit_convention.md).
|
||||
|
||||
The dev team uses `elan` to manage which `lean` toolchain to use
|
||||
locally and `elan` can be used to setup the version of Lean you are
|
||||
manually building. This means you generally do not use `make
|
||||
install`. You use `elan` instead.
|
||||
If you are planning to make any changes that may affect the compilation of Lean itself, e.g. changes to the parser, elaborator, or compiler, you should first read about the [bootstrapping pipeline](bootstrap.md).
|
||||
You should not edit the `stage0` directory except using the commands described in that section when necessary.
|
||||
|
||||
## Development Setup
|
||||
|
||||
You can use any of the [supported editors](../setup.md) for editing
|
||||
the Lean source code. If you set up `elan` as below, opening `src/` as
|
||||
a *workspace folder* should ensure that stage 0 will be used for file
|
||||
in that directory.
|
||||
You can use any of the [supported editors](../setup.md) for editing the Lean source code.
|
||||
If you set up `elan` as below, opening `src/` as a *workspace folder* should ensure that stage 0 (i.e. the stage that first compiles `src/`) will be used for files in that directory.
|
||||
|
||||
## Dev setup using elan
|
||||
### Dev setup using elan
|
||||
|
||||
You can use [`elan`](https://github.com/leanprover/elan) to easily
|
||||
switch between stages and build configurations based on the current
|
||||
directory, both for the `lean`, `leanc`, and `leanmake` binaries in your shell's
|
||||
PATH and inside your editor.
|
||||
|
||||
To install elan, you can do so, without installing a default version of Lean, using
|
||||
To install elan, you can do so, without installing a default version of Lean, using (Unix)
|
||||
|
||||
```bash
|
||||
[Unix]
|
||||
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none
|
||||
|
||||
[Windows]
|
||||
```
|
||||
or (Windows)
|
||||
```
|
||||
curl -O --location https://raw.githubusercontent.com/leanprover/elan/master/elan-init.ps1
|
||||
powershell -f elan-init.ps1 --default-toolchain none
|
||||
del elan-init.ps1
|
||||
|
|
|
|||
|
|
@ -1,8 +1,6 @@
|
|||
# Unit Testing
|
||||
# Test Suite
|
||||
|
||||
You can run the unit tests after completing a build using the following:
|
||||
|
||||
After [building lean](../make/index.md) you can run all the tests using
|
||||
After [building Lean](../make/index.md) you can run all the tests using
|
||||
```
|
||||
cd build/release
|
||||
make test ARGS=-j4
|
||||
|
|
@ -29,10 +27,11 @@ ctest -j 4 --output-on-failure --timeout 300
|
|||
|
||||
To get verbose output from ctest pass the `--verbose` command line
|
||||
option. Test output is normally suppressed and only summary
|
||||
information is displayed. This option will show all test output
|
||||
information is displayed. This option will show all test output.
|
||||
|
||||
Here is the summary of the test source code organization.
|
||||
All these tests are included by [/src/shell/CMakeLists.txt](https://github.com/leanprover/lean4/blob/master/src/shell/CMakeLists.txt):
|
||||
## Test Suite Organization
|
||||
|
||||
All these tests are included by [src/shell/CMakeLists.txt](https://github.com/leanprover/lean4/blob/master/src/shell/CMakeLists.txt):
|
||||
|
||||
- `tests/lean`: contains tests that come equipped with a
|
||||
.lean.expected.out file. The driver script `test_single.sh` runs
|
||||
|
|
@ -87,3 +86,36 @@ All these tests are included by [/src/shell/CMakeLists.txt](https://github.com/l
|
|||
|
||||
- `tests/plugin`: tests that compiled Lean code can be loaded into
|
||||
`lean` via the `--plugin` command line option.
|
||||
|
||||
## Fixing Tests
|
||||
|
||||
When the Lean source code or the standard library are modified, some of the
|
||||
tests break because the produced output is slightly different, and we have
|
||||
to reflect the changes in the `.lean.expected.out` files.
|
||||
We should not blindly copy the new produced output since we may accidentally
|
||||
miss a bug introduced by recent changes.
|
||||
The test suite contains commands that allow us to see what changed in a convenient way.
|
||||
First, we must install [meld](http://meldmerge.org/). On Ubuntu, we can do it by simply executing
|
||||
|
||||
```
|
||||
sudo apt-get install meld
|
||||
```
|
||||
|
||||
Now, suppose `bad_class.lean` test is broken. We can see the problem by going to `test/lean` directory and
|
||||
executing
|
||||
|
||||
```
|
||||
./test_single.sh -i bad_class.lean
|
||||
```
|
||||
|
||||
When the `-i` option is provided, `meld` is automatically invoked
|
||||
whenever there is discrepancy between the produced and expected
|
||||
outputs. `meld` can also be used to repair the problems.
|
||||
|
||||
In Emacs, we can also execute `M-x lean4-diff-test-file` to check/diff the file of the current buffer.
|
||||
To mass-copy all `.produced.out` files to the respective `.expected.out` file, use `tests/lean/copy-produced`.
|
||||
When using the Nix setup, add `--keep-failed` to the `nix build` call and then call
|
||||
```sh
|
||||
tests/lean/copy-produced <build-dir>/source/tests/lean
|
||||
```
|
||||
instead where `<build-dir>` is the path printed out by `nix build`.
|
||||
|
|
|
|||
|
|
@ -46,9 +46,8 @@ 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.
|
||||
|
||||
To install the build, see [Dev setup using
|
||||
elan](../dev/index.md#dev-setup-using-elan).
|
||||
|
||||
You should not usually run `make install` after a successful build.
|
||||
See [Dev setup using elan](../dev/index.md#dev-setup-using-elan) on how to properly set up your editor to use the correct stage depending on the source directory.
|
||||
|
||||
Useful CMake Configuration Settings
|
||||
-----------------------------------
|
||||
|
|
|
|||
|
|
@ -18,8 +18,7 @@ the stdlib.
|
|||
## Installing dependencies
|
||||
|
||||
[The official webpage of MSYS2][msys2] provides one-click installers.
|
||||
Once installed, you should run the "MSYS2 MinGW 64-bit shell" from the start menu.
|
||||
(The one that runs `mingw64.exe`)
|
||||
Once installed, you should run the "MSYS2 MinGW 64-bit shell" from the start menu (the one that runs `mingw64.exe`).
|
||||
Do not run "MSYS2 MSYS" instead!
|
||||
MSYS2 has a package management system, [pacman][pacman], which is used in Arch Linux.
|
||||
|
||||
|
|
|
|||
|
|
@ -10,7 +10,7 @@ Follow the setup in the link above; to open the Lean shell inside a Lean checkou
|
|||
$ nix-shell -A nix
|
||||
```
|
||||
|
||||
On top of the local and remote Nix cache, it helps to we do still rely on CCache as well to make C/C++ build steps incremental, which are atomic steps from Nix's point of view.
|
||||
On top of the local and remote Nix cache, we do still rely on CCache as well to make C/C++ build steps incremental, which are atomic steps from Nix's point of view.
|
||||
To enable CCache, add the following line to the config file mentioned in the setup:
|
||||
```bash
|
||||
extra-sandbox-paths = /nix/var/cache/ccache
|
||||
|
|
@ -35,7 +35,7 @@ The `stage1.` part in each command is optional:
|
|||
```bash
|
||||
nix build .#test # run tests for stage 1
|
||||
nix build . # build stage 1
|
||||
nix build # dito
|
||||
nix build # ditto
|
||||
```
|
||||
|
||||
## Build Process Description
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue