Doc Gen

Generate HTML documentation for mathlib and Lean

Lean HTML documentation generator

A tool to generate documentation for mathlib.


This script is not Windows friendly.

It depends on features of Lean 3.5c added in

pip install -r requirements.txt
rm -rf _target
leanproject up

Make sure that olean files are generated for mathlib in _target, otherwise this will be extremely slow.


./gen_docs will create a directory html with the generated documentation.

If you don't have enough RAM to run ./gen_docs, consider downloading the documentation from here and renaming docs to html.

The links will point to / as the root of the site. I typically host a server from the html directory with python3 -m http.server. If you intend to host the site somewhere else than the root, call for example ./gen_docs -w ''.

gen_docs -l will symlink the css file, so you can edit style.css in the root directory without regenerating anything. This is useful for local development.

Popular Documentation Generator Projects
Popular Hosts Projects
Popular Content Management Categories
Related Searches

Get A Weekly Email With Trending Projects For These Categories
No Spam. Unsubscribe easily at any time.
Local Development
Documentation Generator