The Lean doc folder contains the Lean Manual and is authored in a combination of markdown (*.md) files and literate Lean files. The .lean files are preprocessed using a tool called LeanInk and Alectryon which produces a generated markdown file. We then run mdbook on the result to generate the html pages.


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

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


Using Nix

Building the manual using Nix (which is what the CI does) is as easy as

$ nix build --update-input lean ./doc

You can also open a shell with mdbook for running the commands mentioned below with nix develop ./doc#book. Otherwise, read on.


To build and test the book you have to preprocess the .lean files with Alectryon then use our own fork of the Rust tool named mdbook. We have our own fork of mdBook with the following additional features:

  • Add support for hiding lines in other languages #1339
  • Make mdbook test call the lean compiler to test the snippets.
  • Ability to test a single chapter at a time which is handy when you are working on that chapter. See the --chapter option.

So you need to setup these tools before you can run mdBook.

  1. install Rust which provides you with the cargo tool for building rust packages. Then run the following:

    cargo install --git mdbook
  2. Clone and run lake build then make the resulting binary available to Alectryon using e.g.

    # make `leanInk` available in the current shell
    export PATH=$PWD/build/bin:$PATH
  3. Create a Python 3.10 environment.

  4. Install Alectryon:

    python3 -m pip install git+
  5. Now you are ready to process the *.lean files using Alectryon as follows:

    cd lean4/doc
    alectryon --frontend lean4+markup examples/palindromes.lean --backend webpage -o

    Repeat this for the other .lean files you care about or write a script to process them all.

  6. Now you can build the book using:

    cd lean4/doc
    mdbook build

This will put the HTML in a out folder so you can load out/index.html in your web browser and it should look like

  1. It is also handy to use e.g. mdbook watch in the doc/ folder so that it keeps the html up to date while you are editing.

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

Testing Lean Snippets

You can run the following in the doc/ folder to test all the lean code snippets.

mdbook test

and you can use the --chapter option to test a specific chapter that you are working on:

mdbook test --chapter Array

Use chapter name ? to get a list of all the chapter names.