diff --git a/doc/SUMMARY.md b/doc/SUMMARY.md
index 9c6b306b92..f2bc424987 100644
--- a/doc/SUMMARY.md
+++ b/doc/SUMMARY.md
@@ -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)
\ No newline at end of file
diff --git a/doc/coding_style.md b/doc/coding_style.md
deleted file mode 100644
index 774afebd10..0000000000
--- a/doc/coding_style.md
+++ /dev/null
@@ -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.
diff --git a/doc/dev/bootstrap.md b/doc/dev/bootstrap.md
new file mode 100644
index 0000000000..f4fcb24bc3
--- /dev/null
+++ b/doc/dev/bootstrap.md
@@ -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/`.
\ No newline at end of file
diff --git a/doc/commit_convention.md b/doc/dev/commit_convention.md
similarity index 100%
rename from doc/commit_convention.md
rename to doc/dev/commit_convention.md
diff --git a/doc/dev/cpp_coding_style.md b/doc/dev/cpp_coding_style.md
new file mode 100644
index 0000000000..6cf2aceb40
--- /dev/null
+++ b/doc/dev/cpp_coding_style.md
@@ -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`.
diff --git a/doc/debugging.md b/doc/dev/debugging.md
similarity index 100%
rename from doc/debugging.md
rename to doc/dev/debugging.md
diff --git a/doc/fixing_tests.md b/doc/dev/fixing_tests.md
similarity index 100%
rename from doc/fixing_tests.md
rename to doc/dev/fixing_tests.md
diff --git a/doc/dev/index.md b/doc/dev/index.md
new file mode 100644
index 0000000000..a0976dbcc1
--- /dev/null
+++ b/doc/dev/index.md
@@ -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)`.
diff --git a/doc/mdbook.md b/doc/dev/mdbook.md
similarity index 100%
rename from doc/mdbook.md
rename to doc/dev/mdbook.md
diff --git a/doc/dev/testing.md b/doc/dev/testing.md
new file mode 100644
index 0000000000..0e24cfb04d
--- /dev/null
+++ b/doc/dev/testing.md
@@ -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`
diff --git a/doc/images/code-wsl.png b/doc/images/code-wsl.png
new file mode 100644
index 0000000000..db25e07018
Binary files /dev/null and b/doc/images/code-wsl.png differ
diff --git a/doc/make/emscripten.md b/doc/make/emscripten.md
index 8181b822a2..36c764b2f7 100644
--- a/doc/make/emscripten.md
+++ b/doc/make/emscripten.md
@@ -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
 
diff --git a/doc/make/index.md b/doc/make/index.md
index 21679c96d2..63984f2cf7 100644
--- a/doc/make/index.md
+++ b/doc/make/index.md
@@ -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
 ---------------
diff --git a/doc/make/msvc.md b/doc/make/msvc.md
index 6e585e9c5a..0fcc87c8d6 100644
--- a/doc/make/msvc.md
+++ b/doc/make/msvc.md
@@ -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.
diff --git a/doc/make/msys2.md b/doc/make/msys2.md
index cf3d493c02..b917986205 100644
--- a/doc/make/msys2.md
+++ b/doc/make/msys2.md
@@ -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:
diff --git a/doc/make/nix.md b/doc/make/nix.md
index 5e3b43583c..002afb7f83 100644
--- a/doc/make/nix.md
+++ b/doc/make/nix.md
@@ -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:
diff --git a/doc/make/osx-10.9.md b/doc/make/osx-10.9.md
index 68c7122bdb..301fe55fd9 100644
--- a/doc/make/osx-10.9.md
+++ b/doc/make/osx-10.9.md
@@ -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
+```
\ No newline at end of file
diff --git a/doc/make/ubuntu-16.04.md b/doc/make/ubuntu-16.04.md
index 6b7c7df681..089e910927 100644
--- a/doc/make/ubuntu-16.04.md
+++ b/doc/make/ubuntu-16.04.md
@@ -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
 ```
diff --git a/doc/make/wsl.md b/doc/make/wsl.md
new file mode 100644
index 0000000000..894140a1a8
--- /dev/null
+++ b/doc/make/wsl.md
@@ -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.
\ No newline at end of file
diff --git a/doc/make/wsl2.md b/doc/make/wsl2.md
new file mode 100644
index 0000000000..f86b60582c
--- /dev/null
+++ b/doc/make/wsl2.md
@@ -0,0 +1 @@
+# Windows with WSL