max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc: add wsl setup docs and reorganize a new "dev" folder

Browse source
This commit is contained in:
Chris Lovett 2021-09-23 00:21:39 -07:00 • committed by GitHub
parent 58c938cef8
commit 3a20b6be8a
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
20 changed files with 572 additions and 479 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
doc/SUMMARY.md
View file

@ -55,12 +55,16 @@
# Development
- [Commit Convention](./commit_convention.md)
- [Development Guide](./dev/index.md)
- [Commit Convention](./dev/commit_convention.md)
- [Building Lean](./make/index.md)
- [Ubuntu Setup](./make/ubuntu-16.04.md)
- [macOS Setup](./make/osx-10.9.md)
- [Windows Setup](./make/msys2.md)
- [Windows MSYS2 Setup](./make/msys2.md)
- [Windows with WSL](./make/wsl2.md)
- [Nix Setup (*Experimental*)](./make/nix.md)
- [Building This Manual](./mdbook.md)
- [Fixing Tests](./fixing_tests.md)
- [Debugging](./debugging.md)
- [Unit Testing](./dev/testing.md)
- [Building This Manual](./dev/mdbook.md)
- [Fixing Tests](./dev/fixing_tests.md)
- [Debugging](./dev/debugging.md)
- [C++ Coding Style](./dev/cpp_coding_style.md)

244
doc/coding_style.md
View file

@ -1,244 +0,0 @@
Coding Style
============
[C++11](http://en.wikipedia.org/wiki/C%2B%2B11) features
--------------------------------------------------------
We make 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 bracket.
- Thread local storage.
- Threading facilities.
- Tuple types.
Comments
--------
The comments in the Lean codebase contain
[Doxygen](http://www.stack.nl/~dimitri/doxygen/) commands.
Doxygen is the de facto standard tool for generating documentation from
annotated C++ sources.
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`.
Smart pointers
--------------
We only use `std::shared_ptr` template for class `C` only if we expect
to create only a few objects (< 1000) of class `C`. Otherwise, we
implement our own intrusive smart pointer. For example, the class
`expr` is an intrusive smart pointer to `expr_cell`. We may have
millions of `expr` objects. We say it is intrusive because the
reference counter is stored in `expr_cell`.
We use `std::unique_ptr` to make sure unique resources will be freed
correctly.
Template
--------
We organize template source code using the approach described at http://www.codeproject.com/Articles/3515/How-To-Organize-Template-Source-Code
Idioms
------
We 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
----------
* We use 4 spaces for indentation.
* Class, method, and function names are lower case
We use `_` for composite names. Example: `type_checker`.
* Class/struct fields should start with the prefix `m_`.
Example:
class point {
int m_x;
int m_y;
public:
...
};
* We do **not** use the `#ifndef-#define-#endif` idiom for header files.
Instead we use `#pragma once`.
* We write `type const & v` instead of `const type & v`.
* We use `const` extensively.
* `if-then-else`
The following forms are acceptable:
if (cond) {
...
} else {
...
}
and
if (cond)
statement1;
else
statement2;
In *exceptional cases*, we also use
if (cond) statement;
and
if (cond) statement1; else stament2;
* `if-then-else-if-else`
The following forms are acceptable:
if (cond) {
...
} else if (cond) {
...
} else {
...
}
and
if (cond)
statement1;
else if (cond)
statement2;
else
statement3;
* We frequently format code using extra spaces
For example, we write
environment const & m_env;
cache m_cache;
normalizer m_normalizer;
volatile bool m_interrupted;
instead of
environment const & m_env;
cache m_cache;
normalizer m_normalizer;
volatile bool m_interrupted;
* We use the macro `lean_assert` for assertions.
The macro `lean_assert` is extensively used when writing unit tests.
* Spaces in expressions
We write `a == b` instead of `a==b`.
Similarly, we write `x < y + 1` instead of `x<y+1`.
Google's C++ Style Guide
------------------------
We are using a modified version of [Google's C++ Style Guide][google-style].
We also have our version of Google's style checker [cpplint.py][cpplint].
You can run the checker over the codebase by typing:
make style
If you use Ninja, you can check by ``ninja style``. It is also a part of testcases and can be run by
ctest -R style_check
*Disabled* Features:
- Namespace should be terminated with "namespace"
- At least two spaces is best between code and comments
- Do not use ``dynamic_cast<>``. If you need to cast within a class
hierarchy, use ``static_cast<>`` to upcast. Google doesn't support
RTTI.
- "public:" should be preceded by a blank line
- Missing space before ``{``
- Found C system header after C++ system header. Should be:
environment.h, c system, c++ system, other.
- Labels should always be indented at least one space. If this is
a member-initializer list in a constructor or the base class list in
a class definition, the colon should be on the following line.
- You don't need a ``;`` after a ``}``
- No ``#ifndef`` header guard found
- Streams are highly discouraged.
- Extra space before ``(`` in function call
- Else clause should never be on same line as else
- Extra space before ``)``
- Is this a non-const reference? If so, make const or use a pointer.
- All parameters should be named in a function
- Do not use anonymous constructor notation (e.g., ``{a1, ..., an}``)
Modified Features:
- Add ``#include <list>`` for ``list<>``
=> *Check* ``std::list`` instead of ``list`` because we do have our own ``lean::list`` type.
- Add ``#include <algorithm>`` for copy
=> *Check* ``std::copy`` instead of ``copy`` because we do have our own ``lean::copy`` method.
- Do not use namespace using-directives. Use using-declarations instead.
=> *Allow* this if filename contains "tests/"
- Small and focused functions are preferred: foo()
has xxx non-comment lines (error triggered by exceeding 500 lines).
=> *Allow* this if filename contains "tests/"
- Include the directory when naming .h files
=> *Allow* this if the included filename is "version.h" which is generated by cmake.
[google-style]: http://google-styleguide.googlecode.com/svn/trunk/cppguide.xml
[cpplint]: /src/cmake/Modules/cpplint.py
Git pre-push hook
-----------------
Since [git 1.8.2][git-pre-push-hook], git introduced *pre-push* hook
which is executed *before* actual push operation is performed. Using this,
we can *automatically* run the style checker over the changed files *before*
we push commits to repositories. This is useful because it prevents us
from accidentally pushing the commits which contain style problems.
[git-pre-push-hook]: https://github.com/git/git/blob/master/Documentation/RelNotes/1.8.2.txt
To activate the hook, execute
```bash
ln -s ../../script/pre-push .git/hooks
```
in the project root directory.
You can change the ``CHECKER`` variable in the script if you want to use other
checkers.

122
doc/dev/bootstrap.md Normal file
View file

@ -0,0 +1,122 @@
# Lean Build Bootstrapping
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/
# Bootstrap binary built from stage0/src/.
# We do not use any other files from this directory in further stages.
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`
share/lean/
Makefile # 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
bin/
lean # the Lean compiler & server linked together from the above libraries
leanc # a wrapper around a C compiler supplying search paths etc
leanmake # a wrapper around `make` supplying the Makefile above
stage2/...
stage3/...
```
Stage 0 can be viewed as a blackbox since it does not depend on any local
changes and is equivalent to downloading a bootstrapping binary as done in other
compilers. The build for any other stage starts by building the runtime and
standard library from `src/`, using the `lean` binary from the previous stage in
the latter case, which are then assembled into a new `bin/lean` binary.
Each stage can be built by calling `make stageN` in the root build folder.
Running just `make` will default to stage 1, which is usually sufficient for
testing changes on the test suite or other files outside of the stdlib. However,
it might happen that the stage 1 compiler is not able to load its own stdlib,
e.g. when changing the .olean format: the stage 1 stdlib will use the format
generated by the stage 0 compiler, but the stage 1 compiler will expect the new
format. In this case, we should continue with building and testing stage 2
instead, which will both build and expect the new format. Note that this is only
possible because when building a stage's stdlib, we use the previous compiler
but never load the previous stdlib (since everything is `prelude`). We can also
use stage 2 to test changes in the compiler or other "meta" parts, i.e. changes
that affect the produced (.olean or .c) code, on the stdlib and compiler itself.
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:
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. link that and the current C++ code from `src/` into `stage1/bin/lean`
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`.
`make update-stage0` without `-C` defaults to stage1.
## Further Bootstrapping Complications
As written above, changes in meta code in the current stage usually will only
affect later stages. This is an issue in two specific cases.
* For *non-builtin* meta code such as `notation`s or `macro`s in
`Notation.lean`, we expect changes to affect the current file and all later
files of the same stage immediately, just like outside the stdlib. To ensure
this, we need to build the stage using `-Dinterpreter.prefer_native=false` -
otherwise, when executing a macro, the interpreter would notice that there is
already a native symbol available for this function and run it instead of the
new IR, but the symbol is from the previous stage!
To make matters more complicated, while `false` is a reasonable default
incurring only minor overhead (`ParserDescr`s and simple macros are cheap to
interpret), there are situations where we *need* to set the option to `true`:
when the interpreter is executed from the native code of the previous stage,
the type of the value it computes must be identical to/ABI-compatible with the
type in the previous stage. For example, if we add a new parameter to `Macro`
or reorder constructors in `ParserDescr`, building the stage with the
interpreter will likely fail. Thus we need to set `interpreter.prefer_native`
to `true` in such cases to "freeze" meta code at their versions in the
previous stage; no new meta code should be introduced in this stage. Any
further stages (e.g. after an `update-stage0`) will then need to be compiled
with the flag set to `false` again since they will expect the new signature.
For an example, see https://github.com/leanprover/lean4/commit/da4c46370d85add64ef7ca5e7cc4638b62823fbb.
* For the special case of *quotations*, it is desirable to have changes in
built-in parsers affect them immediately: when the changes in the parser
become active in the next stage, macros implemented via quotations should
generate syntax trees compatible with the new parser, and quotation patterns
in macro and elaborators should be able to match syntax created by the new
parser and macros. Since quotations capture the syntax tree structure during
execution of the current stage and turn it into code for the next stage, we
need to run the current stage's built-in parsers in quotation via the
interpreter for this to work. Caveats:
* Since interpreting full parsers is not nearly as cheap and we rarely change
built-in syntax, this needs to be opted in using `-Dinternal.parseQuotWithCurrentStage=true`.
* The parser needs to be reachable via an `import` statement, otherwise the
version of the previous stage will silently be used.
* Only the parser code (`Parser.fn`) is affected; all metadata such as leading
tokens is taken from the previous stage.
For an example, see https://github.com/leanprover/lean4/commit/f9dcbbddc48ccab22c7674ba20c5f409823b4cc1#diff-371387aed38bb02bf7761084fd9460e4168ae16d1ffe5de041b47d3ad2d22422
(from before the flag defaulted to `false`).
To modify either of these flags both for building and editing the stdlib, adjust
the code in `stage0/src/stdlib_flags.h`. The flags will automatically be reset
on the next `update-stage0` when the file is overwritten with the original
version in `src/`.

0
doc/commit_convention.md → doc/dev/commit_convention.md
View file

155
doc/dev/cpp_coding_style.md Normal file
View file

@ -0,0 +1,155 @@
[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`.

0
doc/debugging.md → doc/dev/debugging.md
View file

0
doc/fixing_tests.md → doc/dev/fixing_tests.md
View file

71
doc/dev/index.md Normal file
View file

@ -0,0 +1,71 @@
# Development Workflow
- [Commit Convention](./commit_convention.md)
- [Building Lean](../make/index.md)
- [Ubuntu Setup](../make/ubuntu-16.04.md)
- [macOS Setup](../make/osx-10.9.md)
- [Windows MSYS2 Setup](../make/msys2.md)
- [Windows with WSL](../make/wsl2.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.
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.
## 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 should also set the `LEAN_SRC_PATH` environment
variable to the path of the `src/` directory to enable
go-to-definition in the stdlib (automatically set when using
`nix-shell`).
## 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/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
```bash
curl https://raw.githubusercontent.com/leanprover/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 `stage1` for everything else (e.g.
tests).
```bash
# in the Lean rootdir
elan toolchain link lean4 build/release/stage1
elan toolchain link lean4-stage0 build/release/stage0
# make `lean` etc. point to stage1 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)`.

0
doc/mdbook.md → doc/dev/mdbook.md
View file

98
doc/dev/testing.md Normal file
View file

@ -0,0 +1,98 @@
# Unit Testing
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
```
cd build/release
make test ARGS=-j4
```
Change the 4 to the maximum number of parallel tests you want to
allow. The best choice is the number of CPU cores on your machine as
the tests are mostly CPU bound. You can find the number of processors
on linux using `nproc` and on Windows it is the `NUMBER_OF_PROCESSORS`
environment variable.
You can run tests after [building a specific stage](bootstrap.md) by
adding the `-C stageN` argument. The default when run as above is stage 1. The
Lean tests will automatically use that stage's corresponding Lean
executables
You can also use `ctest` directly if you are in the right folder. So
to run stage1 tests with a 300 second timeout run this:
```bash
cd build/release/stage1
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
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):
- `tests/lean`: contains tests that come equipped with a
.lean.expected.out file. The driver script `test_single.sh` runs
each test and checks the actual output (*.produced.out) with the
checked in expected output.
- `tests/lean/run`: contains tests that are run through the lean
command line one file at a time. These tests only look for error
codes and do not check the expected output even though output is
produced, it is ignored.
- `tests/lean/interactive`: are designed to test server requests at a
given position in the input file. Each .lean file contains comments
that indicate how to simulate a client request at that position.
using a `--^` point to the line position. Example:
```lean,ignore
open Foo in
theorem tst2 (h : a ≤ b) : a + 2 ≤ b + 2 :=
Bla.
--^ textDocument/completion
```
In this example, the test driver `test_single.sh` will simulate an
auto-completion request at `Bla.`. The expected output is stored in
a .lean.expected.out in the json format that is part of the
[Language Server
Protocol](https://microsoft.github.io/language-server-protocol/).
This can also be used to test the following additional requests:
```
--^ textDocument/hover
--^ textDocument/typeDefinition
--^ textDocument/definition
--^ $/lean/plainGoal
--^ $/lean/plainTermGoal
--^ insert: ...
--^ collectDiagnostics
```
- `tests/lean/server`: Tests more of the Lean `--server` protocol.
There are just a few of them, and it uses .log files containing
JSON.
- `tests/compiler`: contains tests that will run the Lean compiler and
build an executable that is executed and the output is compared to
the .lean.expected.out file. This test also contains a subfolder
`foreign` which shows how to extend Lean using C++.
- `tests/lean/trust0`: tests that run Lean in a mode that Lean doesn't
even trust the .olean files (i.e., trust 0).
- `tests/bench`: contains performance tests.
- `tests/plugin`: tests that compiled Lean code can be loaded into
`lean` via the `--plugin` command line option.
- `tests/leanpkg`: tests the `leanpkg` program, where each sub-folder
is a complete "lean package", including:
- `cyclic`
- `user_ext`
- `user_attr`
- `user_opt`
- `prv`
- `user_attr_app`

BIN
doc/images/code-wsl.png Normal file
View file

Binary file not shown.
Side by side

After

Width:  |  Height:  |  Size: 38 KiB

3
doc/make/emscripten.md
View file

@ -1,5 +1,4 @@
Compiling lean.js via Emscripten
--------------------------------
# Compiling lean.js via Emscripten
First install Emscripten via your distribution's package manager or [download and install it](https://kripken.github.io/emscripten-site/docs/getting_started/downloads.html) yourself. Then build asm.js and WebAssembly binaries using

185
doc/make/index.md
View file

@ -8,9 +8,10 @@ Requirements
Platform-Specific Setup
-----------------------
- [Linux (Ubuntu)](ubuntu.md)
- [Linux (Ubuntu)](ubuntu-16.04.md)
- [Windows (msys2)](msys2.md)
- [Windows (Visual Studio)](msvc.md)
- [Windows (WSL)](wsl.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.
- There is also an [**experimental** setup based purely on Nix](nix.md) that works fundamentally differently from the
@ -54,7 +55,7 @@ below for details. Add `-jN` for an appropriate `N` to `make` for a parallel
build.
To install the build see [Dev setup using
elan](index.md#dev-setup-using-elan) below.
elan](../dev/index.md#dev-setup-using-elan).
Useful CMake Configuration Settings
@ -72,185 +73,7 @@ Pass these along with the `cmake ../..` command.
see also `.github/workflows/ci.yml` for the CI config.
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/
# Bootstrap binary built from stage0/src/.
# We do not use any other files from this directory in further stages.
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`
share/lean/
Makefile # 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
bin/
lean # the Lean compiler & server linked together from the above libraries
leanc # a wrapper around a C compiler supplying search paths etc
leanmake # a wrapper around `make` supplying the Makefile above
stage2/...
stage3/...
```
Stage 0 can be viewed as a blackbox since it does not depend on any local
changes and is equivalent to downloading a bootstrapping binary as done in other
compilers. The build for any other stage starts by building the runtime and
standard library from `src/`, using the `lean` binary from the previous stage in
the latter case, which are then assembled into a new `bin/lean` binary.
Each stage can be built by calling `make stageN` in the root build folder.
Running just `make` will default to stage 1, which is usually sufficient for
testing changes on the test suite or other files outside of the stdlib. However,
it might happen that the stage 1 compiler is not able to load its own stdlib,
e.g. when changing the .olean format: the stage 1 stdlib will use the format
generated by the stage 0 compiler, but the stage 1 compiler will expect the new
format. In this case, we should continue with building and testing stage 2
instead, which will both build and expect the new format. Note that this is only
possible because when building a stage's stdlib, we use the previous compiler
but never load the previous stdlib (since everything is `prelude`). We can also
use stage 2 to test changes in the compiler or other "meta" parts, i.e. changes
that affect the produced (.olean or .c) code, on the stdlib and compiler itself.
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:
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. link that and the current C++ code from `src/` into `stage1/bin/lean`
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`.
`make update-stage0` without `-C` defaults to stage1.
### Further Bootstrapping Complications
As written above, changes in meta code in the current stage usually will only
affect later stages. This is an issue in two specific cases.
* For *non-builtin* meta code such as `notation`s or `macro`s in
`Notation.lean`, we expect changes to affect the current file and all later
files of the same stage immediately, just like outside the stdlib. To ensure
this, we need to build the stage using `-Dinterpreter.prefer_native=false` -
otherwise, when executing a macro, the interpreter would notice that there is
already a native symbol available for this function and run it instead of the
new IR, but the symbol is from the previous stage!
To make matters more complicated, while `false` is a reasonable default
incurring only minor overhead (`ParserDescr`s and simple macros are cheap to
interpret), there are situations where we *need* to set the option to `true`:
when the interpreter is executed from the native code of the previous stage,
the type of the value it computes must be identical to/ABI-compatible with the
type in the previous stage. For example, if we add a new parameter to `Macro`
or reorder constructors in `ParserDescr`, building the stage with the
interpreter will likely fail. Thus we need to set `interpreter.prefer_native`
to `true` in such cases to "freeze" meta code at their versions in the
previous stage; no new meta code should be introduced in this stage. Any
further stages (e.g. after an `update-stage0`) will then need to be compiled
with the flag set to `false` again since they will expect the new signature.
For an example, see https://github.com/leanprover/lean4/commit/da4c46370d85add64ef7ca5e7cc4638b62823fbb.
* For the special case of *quotations*, it is desirable to have changes in
built-in parsers affect them immediately: when the changes in the parser
become active in the next stage, macros implemented via quotations should
generate syntax trees compatible with the new parser, and quotation patterns
in macro and elaborators should be able to match syntax created by the new
parser and macros. Since quotations capture the syntax tree structure during
execution of the current stage and turn it into code for the next stage, we
need to run the current stage's built-in parsers in quotation via the
interpreter for this to work. Caveats:
* Since interpreting full parsers is not nearly as cheap and we rarely change
built-in syntax, this needs to be opted in using `-Dinternal.parseQuotWithCurrentStage=true`.
* The parser needs to be reachable via an `import` statement, otherwise the
version of the previous stage will silently be used.
* Only the parser code (`Parser.fn`) is affected; all metadata such as leading
tokens is taken from the previous stage.
For an example, see https://github.com/leanprover/lean4/commit/f9dcbbddc48ccab22c7674ba20c5f409823b4cc1#diff-371387aed38bb02bf7761084fd9460e4168ae16d1ffe5de041b47d3ad2d22422
(from before the flag defaulted to `false`).
To modify either of these flags both for building and editing the stdlib, adjust
the code in `stage0/src/stdlib_flags.h`. The flags will automatically be reset
on the next `update-stage0` when the file is overwritten with the original
version in `src/`.
Development Setup
-----------------
After building a stage, you can invoke `make -C stageN test` (or, even better,
`make -C stageN test ARGS=-jN` to make `ctest` parallel) to run the Lean test suite.
`make test` without `-C` defaults to stage1. 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/leanprover/elan), see the next section.
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 should also set the
`LEAN_SRC_PATH` environment variable to the path of the `src/` directory to enable
go-to-definition in the stdlib (automatically set when using `nix-shell`).
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/leanmake` binaries in your shell's PATH and inside your editor.
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/leanprover/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 `stage1` for everything else (e.g. tests).
```
# in the Lean rootdir
elan toolchain link lean4 build/release/stage1
elan toolchain link lean4-stage0 build/release/stage0
# make `lean` etc. point to stage1 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)`.
redundant builds, especially after stage 0 has been updated.
Troubleshooting
---------------

17
doc/make/msvc.md
View file

@ -1,10 +1,10 @@
Compiling Lean with Visual Studio
---------------------------------
# Compiling Lean with Visual Studio
WARNING: Compiling Lean with Visual Studio doesn't currently work.
There's an ongoing effort to port Lean to Visual Studio.
The instructions below are for VS 2017.
In the meantime you can use [MSYS2](msys2.md) or [WSL](wsl.md).
## Installing dependencies
@ -20,15 +20,14 @@ In each of the targets, add the following snippet (i.e., after every
`ctestCommandArgs`):
```json
"variables": [
{
"name": "CMAKE_TOOLCHAIN_FILE",
"value": "C:\\path\\to\\vcpkg\\scripts\\buildsystems\\vcpkg.cmake"
}
]
"variables": [
{
"name": "CMAKE_TOOLCHAIN_FILE",
"value": "C:\\path\\to\\vcpkg\\scripts\\buildsystems\\vcpkg.cmake"
}
]
```
## Enable Intellisense
In Visual Studio, press Ctrl+Q and type `CppProperties.json` and press Enter.

17
doc/make/msys2.md
View file

@ -1,13 +1,13 @@
[msys2]: http://msys2.github.io
[pacman]: https://wiki.archlinux.org/index.php/pacman
Lean for Windows
----------------
# Lean for Windows
A native Lean binary for Windows can be generated using [MSYS2][msys2].
It is easy to install all dependencies, it produces native
64/32-binaries, and supports a C++14 compiler.
An alternative to MSYS2 is to use [Lean in Windows WSL](wsl.md).
## Installing dependencies
@ -26,19 +26,22 @@ pacman -S make python mingw-w64-x86_64-cmake mingw-w64-x86_64-clang mingw-w64-x8
You should now be able to run these commands:
```bash
gcc --version
clang --version
cmake --version
```
Then follow the [generic build instructions](index.md) in the MSYS2
MinGW shell, using `cmake ../.. -G "Unix Makefiles"` instead of `cmake
../..`. This ensures that cmake will call `sh` instead of `cmd.exe`
for script tasks.
MinGW shell, using:
```
cmake ../.. -G "Unix Makefiles" -DCMAKE_C_COMPILER=clang -DCMAKE_CXX_COMPILER=clang++
```
instead of `cmake ../..`. This ensures that cmake will call `sh` instead of `cmd.exe`
for script tasks and it will use the clang compiler instead of gcc, which is required.
## Install lean
Follow the steps in [Dev setup using
elan](index.md#dev-setup-using-elan) regarding installation of the
elan](../dev/index.md#dev-setup-using-elan) regarding installation of the
bits you just built. Note that in an msys2 environment `elan-init.sh`
reports you need to add `%USERPROFILE%\.elan\bin` to your path, but of
course in msys2 that needs to be a valid linux style path, like this:

14
doc/make/nix.md
View file

@ -1,6 +1,8 @@
# Building with Nix
While [Nix](https://nixos.org/nix/) can be used to quickly open a shell with all dependencies for the [standard setup](index.md) installed, the user-facing [Nix Setup](../setup.md#nix-setup) can also be used to work *on* Lean.
# Setup
## Setup
Follow the setup in the link above; to open the Lean shell inside a Lean checkout, you can also use
```bash
@ -20,7 +22,7 @@ sudo mkdir -m0770 -p /nix/var/cache/ccache
nix shell .#nixpkgs.coreutils -c sudo chown --reference=/nix/store /nix/var/cache/ccache
```
# Basic Build Commands
## Basic Build Commands
From the Lean root directory inside the Lean shell:
```bash
@ -36,7 +38,7 @@ nix build . # build stage 1
nix build # dito
```
# Build Process Description
## Build Process Description
The Nix build process conceptually works the same as described in [Lean Build Pipeline](index.md#lean-build-pipeline).
However, there are two important differences in practice apart from the standard Nix properties (hermeneutic, reproducible builds stored in a global hash-indexed store etc.):
@ -45,7 +47,7 @@ This is actually a general property of Nix flakes, and has the benefit of making
* Only files reachable from `src/Lean.lean` are compiled.
This is because modules are discovered not from a directory listing anymore but by recursively compiling all dependencies of that top module.
# Editor Integration
## Editor Integration
As in the standard Nix setup.
After adding `src/` as an LSP workspace, it should automatically fall back to using stage 0 in there.
@ -55,7 +57,7 @@ there is no mutable directory incrementally filled by the build that we could po
Instead, `emacs-dev` will gather the individual dependency outputs from the Nix store when checking a file -- and build them on the fly when necessary.
However, it will only ever load changes saved to disk, not ones opened in other buffers.
# Other Fun Stuff to Do with Nix
## Other Fun Stuff to Do with Nix
Open Emacs with Lean set up from an arbitrary commit (without even cloning Lean beforehand... if your Nix is new enough):
```bash
@ -90,7 +92,7 @@ This setup will inadvertently change your `flake.lock` file, which you can rever
...more surely to come...
# Debugging
## Debugging
Since Nix copies all source files before compilation, you will need to map debug symbols back to the original path using `set substitute-path` in GDB.
For example, for a build on Linux with the Nix sandbox activated:

42
doc/make/osx-10.9.md
View file

@ -1,11 +1,10 @@
Install Packages on OS X 10.9
-----------------------------
# Install Packages on OS X 10.9
We assume that you are using [homebrew][homebrew] as a package manager.
[homebrew]: http://brew.sh
Compilers
---------
## Compilers
You need a C++11-compatible compiler to build Lean. As of November
2014, you have three options:
@ -18,29 +17,30 @@ We recommend to use Apple's clang++ because it is pre-shipped with OS
X and requires no further installation.
To install gcc-4.9.1 via homebrew, please execute:
brew install gcc
```bash
brew install gcc
```
To install clang++-3.5 via homebrew, please execute:
brew install llvm --with-clang --with-asan
```bash
brew install llvm --with-clang --with-asan
```
To use compilers other than the default one (Apple's clang++), you
need to use `-DCMAKE_CXX_COMPILER` option to specify the compiler
that you want to use when you run `cmake`. For example, do the
following to use `g++`.
```bash
cmake -DCMAKE_CXX_COMPILER=g++ ...
```
cmake -DCMAKE_CXX_COMPILER=g++ ...
## Required Packages: CMake, GMP
```bash
brew install cmake
brew install gmp
```
Required Packages: CMake, GMP
---------------------
## Recommended Packages: CCache
brew install cmake
brew install gmp
Recommended Packages: CCache
----------------------------
brew install ccache
```bash
brew install ccache
```

12
doc/make/ubuntu-16.04.md
View file

@ -1,8 +1,12 @@
Installing Lean on Ubuntu 16.04
-------------------------------
# Installing Lean on Ubuntu 16.04
### Basic packages
## Build Dependencies
Please ensure you have the following build tools available and then
follow the [generic build instructions](index.md).
## Basic packages
```bash
sudo apt-get install git libgmp-dev cmake ccache
sudo apt-get install git libgmp-dev cmake ccache gcc-10 g++-10
```

56
doc/make/wsl.md Normal file
View file

@ -0,0 +1,56 @@
[vscode]: https://code.visualstudio.com/Download
[wsl]: https://docs.microsoft.com/en-us/windows/wsl/install-win10
# Lean in Windows WSL
As an alternative to the [MSYS2](msys2.md) setup you can also use the
[Windows Subsystem for Linux][wsl] to build Lean there, but edit and
debug using [Visual Studio Code][vscode] in Windows.
For the most part setup in WSL is the same as
[Ubuntu](Ubuntu-16.04.md). This document provides additional
information on how to setup Windows Visual Studio Code remote
debugging into your WSL environment using the lean extension running
in WSL.
It is recommended that you setup Ubuntu in [WSL
2](https://docs.microsoft.com/en-us/windows/wsl/compare-versions).
Then follow the [Dev setup using elan](../dev/index.md#dev-setup-using-elan).
## Visual Studio Code setup on Windows
Install [Visual Studio Code][vscode] on Windows. Install the VS Code
`Remote Development` extension from Microsoft. This extension
includes the `Remote - WSL` extension. Install the lean4 extension but
into the WSL using: `Install in WSL: Ubuntu`
Type `Ctrl+Shift+P` and select `Remote-WSL: Open Folder in WSL...` to
open a folder containing your hello world lean package.
When everything is working you should see this:
![screenshot](../images/code-wsl.png)
with a functioning infoview, syntax coloring and tooltips.
## Troubleshooting
**Connection to server is erroring. Shutting down server.**
If your `leanpkg` has a `build` folder try deleting it. Lean .olean
binaries are not cross platform so if the binaries were copied from a
different platform they need to be deleted so that the new build is
created for your platform.
**Logs are showing up with a windows file path**
Check that you have not set a windows path in your
`lean4.serverLogging.path` Visual Studio Code setting. it is best if
this setting is set as follows:
```json
"lean4.serverLogging.path": "logs"
```
This will result in a logs folder being created inside your lean
package folder in the WSL file system.

1
doc/make/wsl2.md Normal file
View file

@ -0,0 +1 @@
# Windows with WSL