Skip to content
lean doc_string latex generator
Branch: master
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Type Name Latest commit message Commit time
Failed to load latest commit information.


lean doc_string latex generator

This is a somewhat experimental documentation generator for lean source files. In order to avoid parsing lean sources it relies on extracting the documentation from lean bytecode.

Due to the above, you must your compile sources with lean first. Documentation will then be generated from the .olean file which lean produces.

See Lumpy.toml for an example configuration file.


The primary motivation is to make it easy to install and use. as such it comes with a TeX renderer tectonic which automatically downloads any latex packages and fonts needed to render the document.

Syntax highlighting will not shell out to any external tools that need to be installed seperately.


In it's current state, this automatic downloading results in the first run taking quite a bit of time while it fills in the cache. During this time there is currently no output. This wait can be avoided by not using the pdf output format.


  1. install rust
  2. install harfbuzz 1.4 or later is required. harfbuzz needs to be built with libicu and graphite2 support. With ubuntu apt-get install libharfbuzz-dev On fedora dnf install harfbuzz-devel should suffice.
  3. cargo install --git


  • Add a Lumpy.toml next to your leanpkg.toml
  • leanpkg build as normal
  • run lumpy-leandoc
  • example output examples.pdf

List of features:

  • Syntax highlighting via syntect
  • Tex -> PDF generation via tectonic
  • Markdown via pulldown_cmark
  • HTML output (work in progress)
You can’t perform that action at this time.