Writing about Lean takes many forms, including but not limited to:
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:
Please consult the in-progress Verso manual (HTML, PDF) for further details. Today, Verso is usable for running a website and blog, while the other genres are still under development.
Verso's design is primarily inspired by Scribble and Sphinx.
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.
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.
The examples directory contains example documents
built with the default Verso genres.
A minimal example of a Verso genre that includes nontrivial
cross-references can be found in
examples/custom-genre. To build and run
it, with the output being placed in ./index.html, use:
lake exe simplepageTo build the example website and place the results in
_out/examples/demosite, run:
lake build
lake exe demosite --output _out/examples/demositeTo view the output, a local server will be needed. One way to get such a server is to use the one from the Python standard library, e.g.
python3 -m http.server 8800 --directory _out/examples/demosite &after which http://localhost:8800/ will show the generated site.
The textbook example is both an example that can serve as a template for a textbook project in Verso and a place where features can be developed for upstreaming into the manual genre proper.
To build the example website and place the results in
_out/examples/demosite, run:
lake build
lake exe demotextbook --output _out/examples/demotextbookTo view the output, a local server will be needed. One way to get such a server is to use the one from the Python standard library, e.g.
python3 -m http.server 8880 --directory _out/examples/demotextbook/html-single &after which http://localhost:8880/ will show the generated site.
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.