Writing Documentation in Lean with Verso🔗

All of these genres have common concerns, such as displaying Lean code, including tests to prevent bit-rot of the text, and linking to other resources. However, they are also very different. Some have a very linear structure, while others combine date-based content with an unordered set of pages. Some should generate highly interactive output, while others should generate PDFs that can be turned into published papers books.

Verso consists of the following components:

Markup language

Verso's markup language is a simplified variant of Markdown. It is also an alternative concrete syntax for Lean itself, so Verso documents are just Lean files. Just as TeX, Sphinx, and Scribble allow their languages to be extended using their own programming languages, Verso's markup language is extensible. Define a Lean function at the top of a file, and use it in the text of that very same file.

Extensible document structure

All Verso documents can contain a set of common elements, such as paragraphs, emphasized text, or images. They also share a hierarchical structure of sections and subsections. These types are extensible by individual genres.

Elaboration and rendering framework

Verso provides a shared paradigm for converting text written by an author into readable output. Different genres will produce different output formats, but they don't need to reinvent the wheel in order to resolve cross-references, and they can benefit from shared libraries for producing output in various formats.

Cross-reference management

Verso includes a common paradigm for representing the documented items, and a format for sharing cross-reference databases between genres that emit HTML, which enables links and cross-references to be automatically inserted and maintained.

Lean rendering

Verso includes facilities for elaborating and displaying Lean code in documents. In HTML output, this code is rendered with toggleable proof states, hovers, and hyperlinks. It's also highlighted accurately, which is impossible with regexp-based highlighting due to Lean's syntactic extensibility.

The SubVerso helper library allows Verso documents to process Lean code written in any version of Lean, starting with 4.0.0. This makes it possible to write a document that compares and contrasts versions, or to decouple upgrades to the Lean version used in a project from the Lean version used in the document that describes it.

Utility libraries

Verso includes utility libraries that can be used by genres to provide features such as full-text search of HTML content. These libraries have no additional build-time dependencies, avoiding the complications of staying up to date with multiple library ecosystems at once.