Writing about Lean takes many forms, including but not limited to:

• Instructional books such as Theorem Proving in Lean, Functional Programming in Lean, and Mathematics in Lean
• Software documentation, such as the Lean users' manual
• In-source API documentation that is both displayed in IDEs and included in larger documents
• Descriptions of formalization efforts that connect the formal artifact to mathematical text and guide the formalization, such as those made with Blueprint
• Web sites and blog posts
• Research papers in mathematics and computer science that use Lean formalizations in some essential way

Each of these genres needs different tool support than the others, and many different ways of writing about Lean have come into existence, including LeanInk, customizations to mdbook and Sphinx, bespoke Python document management scripts, and doc-gen. But many of these tools share overlapping concerns: most want to include accurately highlighted Lean source code, include links to official descriptions of Lean features, and have internal hyperlinking.

Verso is a collection of libraries for representing documents in Lean paired with an alternative concrete syntax that allows them to be written in something very much like Markdown. Documents written in Verso can make full use of the Lean metaprogramming API to create arbitrary new features, and these features can be made portable between genres. The goals of the project are:

• Be a pleasant tool with which it is enjoyable to write
• Solid IDE support
• Support all of the above genres, with the ability for users to add their own genres
• Empower users to conveniently add their own features to the documentation language
• Enable but not require extensions to be usable in multiple genres

Verso's design is primarily inspired by Scribble and Sphinx.

The verso-templates repository contains templates that can serve as a starting point for Verso-based projects.

The in-progress Verso manual describes the Verso markup language and partially documents the built-in genres. Today, Verso is usable for running a website and blog and for writing long-form technical documentation, such as the Lean language reference.

The workflow described in this section helps Verso development work well with the automation surrounding Lean releases. Please follow it! In the past, the main branch tracked upstream Lean closely, but these procedures make it easier to coordinate PRs across many repositories.

When a Lean release is created, a correponding tag for the compatible version of Verso is also created. For example, the v4.19.0 tag should be used for projects that are built in Lean 4.19.0.

The two most important branches are main and nightly-testing. The main branch of this repository is intended to work with releases or release candidates of Lean, while nightly-testing tracks Lean nightlies. When a Lean release candidate is created, nightly-testing is made to work with it, and then its commits are rebased onto main. When the corresponding release is created, the toolchain file on main is updated and the tag is created. To the extent possible, development occurs on main; it is regularly merged into nightly-testing.

When a Lean release occurs, the adaptation changes are squash-merged into main before the tag is created.

The project is currently undergoing change at a rapid pace. If you'd like to contribute, please get in touch with David Thrane Christiansen and discuss your plans ahead of time, as there is not presently much extra time to onboard and supervise new contributors. This may change as the project matures.

However, one goal of the project is that users should be able to implement their own extensions without needing to modify the Verso libraries. If you've attempted to implement your desired feature as an extension and run into a limitation, please open an issue so we can try to make the system more extensible.

To generate the Verso documentation for Verso itself, run generate.sh.

The title of the book being written in the manual genre can be displayed either at the top of the screen or in the table of contents, depending on screen width. Books with long titles may wish to add a threshold at which the title moves to the table of contents using the following CSS:

/* Move the title from the header to the toc when there is not enough room. */
@media screen and (max-width: 1200px) {
    .toc-title {
        display: block;
    }

    .header-title {
        display: none;
    }
}

Vary the value 1200px until there's space for the title. This CSS should be saved in a served static file and added to the extraCss field in the config parameter to manualMain.

Because Lean's parser is extensible, regular-expression-based syntax highlighting is incapable of accurately identifying keywords or other tokens. Verso includes libraries that can be used to include accurately highlighted Lean code in documents, with support for generating HTML with rich annotations. In particular, tactic proofs are annotated with their proof states, so the proof can be understood without having to open the file in a full Lean environment.

The user interface used to implement the display of proof states is inspired by the excellent Alectryon by Clément Pit-Claudel.

Experimental

In genres that support it, Verso allows linking to other Verso documents based on semantic information about what is being linked to, rather than specific URLs. For example, it's possible to link to "the documentation for Monad" rather than https://example.com/docs/lib/#Monad. To support this, Verso emits a cross-referencing database that describes the available link targets.

Documented information is organized into domains, which are essentially namespaces. Documents may define whatever domains they like, and some are provided with Verso. For instance, domains might be "compiler options" or "constant names" or "syntax categories", but they might also be "chapters and sections", "technical terminology", or topics specific to a given document such as "biographies of historical mathematicians".

Domains contain objects, which are identified by a canonical name. For constants, the canonical name is their fully-qualified name in the environment, while for technical terminology, it's a normalized form of the term with plural markers removed. Objects may additionally have arbitrary metadata associated with them, such as the titles of sections or their position in a table of contents.

Some Verso genres that produce HTML emit a file xref.json in the root of the site. These are the genres that support incoming cross-references. In a verso project, a site that should be linked to is referred to as a remote, by analogy to Git remotes.

To link to other Verso documents, do the following:

1. Create a configuration file that describes the remotes to be used (see later in this section for an example). It should be called verso-sources.json and be in the same directory as the lean-toolchain file.
2. Run lake exe verso sync to download a local mirror of the remote's cross-reference information.
3. Use the configured name for the remote in the ref role to link to it, e.g. {ref "canonicalName" (remote := "lean-reference")}[link text]

Each remote has an update frequency. When building a document, if the remote is configured to be updated automatically and hasn't been updated in the specified duration, its cross-references are fetched. verso sync always updates remotes.

When the structure of a remote document changes, but the documented objects are still present, then rebuilding the current document is sufficient to fix all broken links. If two documents depend on each other, then this process may need to be run on both. If documented objects are removed, then it is an error.

Downloaded remote information is stored in .verso in the project root. The file verso-xref.json contains the local copy of each remote's cross-reference database, while verso-xref-manifest.json tracks when each was updated.

Configuration files are presently JSON, but the plan is to move them to TOML. While JSON does not support comments, this example file includes them for explanation:

{
    "version": 0, // Version specifier for the configuration file format
    // Configured remotes. Keys are their internal names, used by the author.
    "sources": {
        "manual": {
            // The root of the source. xref.json should be here, and all
            // links will be relative to this:
            "root": "https://lean-lang.org/doc/reference/latest/",
            // How often should it be updated?
            // * "manual" means only when running verso sync,
            // * {"days": N} means every N days
            "updateFrequency": "manual",
            // Ultra-short name shown to readers to disambiguate link texts
            // (e.g. when linking to multiple versions of the same document)
            "shortName": "latest",
            // Longer name shown to readers to explain links
            "longName": "Lean Language Reference"
        }
    }
}

Verso includes an experimental Lean-to-HTML renderer that will convert Lean code to HTML. This HTML includes hovers, clickable "go to definition" links, a search function, and rendered intermediate proof states.

To use this in your project:

1. Add Verso as a package dependency.

   If you're using a lakefile.toml configuration, that looks like this:

   [[require]]
   name = "verso"
   git = "https://github.com/leanprover/verso.git"
   rev = "latest"

   If you're using a lakefile.lean configuration, that looks like this:

   require verso from git "https://github.com/leanprover/verso.git"@"latest"

   In either case, you probably want to replace "latest" with the version of Lean you're using: if your lean-toolchain file contains leanprover/lean4:v4.25.0, then you should replace "latest" with "v4.25.0".

2. Generate literate program data from your Lean libraries or modules by building their literate facet. For library MyLib, run:

   lake build MyLib:literate
   

   This generates files in the folder .lake/build/literate

3. Generate HTML from this literate program data. To put the HTML in a directory named html, run:

   lake exe verso-html .lake/build/literate html
   

You can preview the resulting files by running python3 -m http.server 8000 -d html and pointing a web browser to http://localhost:8000/

In this output, Verso docstrings and moduledocs are rendered. Setting doc.verso to true enables these in source files.

The main tests can be run using lake test.

Additionally, some aspects of Verso's JavaScript can be tested using Playwright, a Python browser testing framework. These tests can be found in the browser-tests directory.

To run them, first install uv if you don't have it. Depending on the platform, one of these commands may do the trick:

$ curl -LsSf https://astral.sh/uv/install.sh | sh

$ brew install uv

Then, in the browser-tests directory, install the browser testing engines used by Playwright:

$ cd browser-tests
$ uv run --extra test playwright install chromium firefox

The browser tests run against Verso's own user manual. The first step is to generate it by running ./generate.sh.

Next, run the tests. From the project root, use this command:

$ uv run --project browser-tests --extra test pytest browser-tests -v

From within the browser-tests directory, --project is unnecessary:

$ cd browser-tests
$ uv run --extra test pytest . -v

The test runner accepts a number of parameters. The site's output directory can be set using --site-dir:

$ uv run --project browser-tests --extra test pytest browser-tests --site-dir=dist -v

By default, the script runs a local web server, picking an available port. If this fails, or to force a particular port for some other reason, use the --port option:

$ uv run --project browser-tests --extra test pytest browser-tests --port=3000 -v

To use an existing server, pass --server:

$ uv run --project browser-tests --extra test pytest browser-tests --server-url=http://localhost:4000 -v

To use only one browser engine, pass -k:

$ uv run --project browser-tests --extra test pytest browser-tests -v -k "chromium"

Commits to the main branch will reformat all eligible files (HTML, CSS, JavaScript, and Markdown) with Prettier. There are Prettier extensions for VS Code and for VSCodium that you can use to format your PRs, and if you have npm installed then you can format code from the command line with

npx prettier --write .

It is also possible to run the Prettier GitHub action to format code for an branch without having Prettier installed; the action will run prettier and commit the formatted results.

TL;DR: push a tag of the form vX.Y.Z onto the commit that should be released as the manual for that version, and the rest is automatic.

Deployment happens in GitHub Actions, in response to certain tags being pushed. Because the latest version of the GH action file will always be used, and we want to be able to mutate tags to re-deploy old manual versions (e.g. to update CSS for consistent look and feel while keeping content version-accurate), the steps of the workflow that might change are captured in scripts that are versioned along with the code.

The files are:

• deploy/prep.sh is used to set up the build, installing OS-level dependencies.

• deploy/build.sh is used to build the executable that generates the manual.

• deploy/generate.sh builds the manual, saving it in _out/html-multi and packaging release assets.

• deploy/release.py puts the generated HTML in the right place on a new commit on the deploy branch.

• deploy/release_utils.py contains shared utilities used by both Python scripts (version parsing, version comparison, git helpers).

Everything above is what needs to happen specifically to the single version of the documentation that is being updated in the course of the deploy. There is one further step, which is computing the desired state of the final postdeploy branch from the state in the deploy branch. This is done by the script overlay.py, which is triggered by pushes to deploy, and therefore runs at branch main rather than at the tag being pushed.

• deploy/overlay.py processes deploy → postdeploy.

The goal is to have versioned snapshots of the user's guide, with a structure like:

• https://verso.lean-lang.org/doc/latest/ — latest version
• https://verso.lean-lang.org/doc/stable/ — latest stable version
• https://verso.lean-lang.org/doc/4.29.0/ — guide for v4.29.0
• https://verso.lean-lang.org/doc/4.29.0-rc1/ — guide for v4.29.0-rc1

and so forth. The root URL shows an index of all available versions.

Orphan branches deploy and postdeploy contain the versioned content. For example, the deploy branch might contain:

• /4.29.0-rc1/ — built HTML for 4.29.0-rc1
• /4.29.0/ — built HTML for 4.29.0
• /4.28.0/ — built HTML for 4.28.0
• /latest/ — copy of /4.29.0/ (the most recent version)
• /stable/ — copy of /4.29.0/ (the most recent non-RC version)
• /index.html — root page listing all versions

The latest and stable directories are full copies rather than symlinks because Netlify deployment doesn't support symlinks.

The release.py script is responsible for updating this structure. It takes the generated HTML directory, the version number, the commit SHA, and the deployment branch name as arguments, and then does the following:

1. It copies the HTML to the branch (deleting an existing directory first if needed).
2. It stamps every HTML file with a comment containing the source commit SHA and a UTC timestamp.
3. It updates the latest directory to be a copy of the most recent version, with all numbered releases being considered more recent than any nightly and real releases being more recent than their RCs.
4. It updates the stable directory to be a copy of the most recent non-RC version.
5. It generates a root index.html listing all available versions.
6. It commits the changes to the deployment branch, then switches back to the original branch.

A successful push to deploy triggers a GH action that runs the overlay.py script, which creates commits to postdeploy (based on deploy). These commits include all desired overlays.

A successful push to postdeploy triggers a GH Action which publishes the content to Netlify.

We might have named the two branches predeploy and deploy, but chose instead deploy and postdeploy so that we could leave unchanged any older tags that have workflows emitting commits to deploy.

The script overlay.py computes postdeploy from deploy any time deploy changes. Its purpose is to add metadata or make in-place changes to deployed content that is best thought of as a unified overlay on top of the data that exists at the historical version tags.

Currently-applied overlays:

• noindex meta tag: Added to every HTML file in every version directory except latest/. This prevents search engines from indexing old versions.
• Canonical URL: Added to every HTML file, pointing to the corresponding page under latest/. This tells search engines where the authoritative version lives.
• Unicode input JS files: The vendored Unicode input files (unicode-input.min.js and unicode-input-component.min.js) in every version's -verso-search/ directory are replaced with the versions from main at the time of deployment. This ensures all deployed versions use the latest Unicode input implementation.
• Statistics HTML: The contents of static-web/stats.html from main are injected as the last element of <head> in every HTML file in every version directory. This allows site-wide statistics or analytics code to be updated without rebuilding old versions.

Examples of additional overlays we might add in the future:

• global CSS changes across all versions, for consistency
• banners appended to sufficiently old versions describing how they are deprecated and unsupported

Interactions between overlays created by overlay.py and manual versions should be carefully considered to ensure backwards-compatibility.

An overlay that simply injects a <div> inside old versions is relatively safe, because the document being injected into doesn't need to know about the injection. However, if a document depends rigidly on the presence of data created by the overlay mechanism, a problem could occur if the overlay changes to not produce that data in the future.

Therefore we can be careful on both sides:

• overlays should, ideally, as time goes on, only monotonically produce more data, e.g. it should only add fields to injected javascript values and avoid changing the contract of existing fields.
• documents should, ideally, fail gracefully if injected data they expect to exist is missing

To test overlay.py locally before pushing, do the following.

• Ensure the deployment branches exist locally.
• You'll probably want to do

git fetch
git checkout deploy
git reset --hard remotes/upstream/deploy
git checkout postdeploy
git reset --hard remotes/upstream/postdeploy

• From the repository checkout directory, on branch main, from a clean working directory (i.e. make sure to commit any changes you've made) run

python3 -B deploy/overlay.py . deploy postdeploy

• Inspect whatever postdeploy results you're interested in, e.g.

git show postdeploy:4.29.0-rc1/index.html
# Expect to see <meta name="robots" content="noindex">

git show postdeploy:latest/index.html
# Expect to *not* see <meta name="robots" content="noindex">

Verso is licensed under the Apache license - please see the file LICENSE for details.

Verso additionally includes third-party software made available under the MIT license. These components, and their copyright and licensing information, are in the vendored-js directory.