Settings

We are using the following settings while editing the markdown docs.

{
    "files.insertFinalNewline": true,
    "files.trimTrailingWhitespace": true,
    "[markdown]": {
        "rewrap.wrappingColumn": 70
    }
}

Build

This manual is generated by mdBook. We are currently using a fork of it for the following additional features:

• Add support for hiding lines in other languages #1339
• Replace calling rustdoc --test from mdbook test with ./test

To build this manual, first install the fork via

cargo install --git https://github.com/leanprover/mdBook mdbook

Then use e.g. mdbook watch in the doc/ folder:

cd doc
mdbook watch --open  # opens the output in `out/` in your default browser

Run mdbook test to test all lean code blocks.

Using the Nix setup, you can instead open a shell with the mdBook fork downloaded from our binary cache:

nix develop .#doc