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
frommdbook 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