Skip to content

Building and maintaining the documentation

The site has two parts:

  • Handbook and guides: Markdown in docs/, rendered by MkDocs Material with MathJax for formulas.
  • API: generated by doc-gen4 from the Lean library and its imports, using the separate docbuild/ Lake project.

The public site follows main. Every handbook page records the source revision, and theorem source links are pinned to that revision. The existing release tags are not moved when the documentation changes.

Preview the handbook

Install Python 3.12 or newer, then from the repository root run:

python -m pip install -r docs/requirements.txt
python -m mkdocs serve

The handbook is available at the local address printed by MkDocs. API links need the full documentation build below; a handbook-only preview does not create the Lean reference pages.

Build the complete site

Use the repository's pinned Lean toolchain. First fetch the mathlib cache and build the library:

lake exe cache get
lake build

Then build the API using the committed documentation manifest:

cd docbuild
lake build Copula:docs
cd ..
python -m mkdocs build --strict
python scripts/assemble_docs.py
python scripts/check_docs.py
python -m http.server 8000 --directory site

The complete site is at http://localhost:8000. Serve it over HTTP: API search loads data files and will not work correctly through a file:// URL. The first API build documents imported dependencies as well as Copula and can take considerably longer than a normal library build.

Add a theorem to the handbook

  1. Add an entry to docs/theorems.json with the full Lean declaration name, defining module, and a short mathematical title.
  2. Put a reference marker such as {{ lean:ordinal-unique }} beneath the mathematical statement in a handbook chapter. The renderer produces the formal-statement and source links automatically.
  3. State every relevant hypothesis, including parameter ranges, dimension, conditioning direction, and any continuity or atomlessness requirement.
  4. Build the full site. The checker verifies declaration anchors against generated API pages, checks handbook links, and requires API output for every Copula source module.

The prose is maintained by authors. Lean checks the linked formal proofs; link validation does not prove that an English paraphrase is equivalent to its formal statement.

Update documentation dependencies

docbuild/lean-toolchain must match the root lean-toolchain. Pin doc-gen4 to the matching Lean release, then update and commit its manifest:

cd docbuild
MATHLIB_NO_CACHE_ON_UPDATE=1 lake update doc-gen4

In PowerShell, set $env:MATHLIB_NO_CACHE_ON_UPDATE='1' before running lake update doc-gen4. After changing the library's dependencies, also run lake update copula in docbuild/ and commit the updated manifest. The checker verifies that the shared dependencies have matching revisions.

Python dependencies are pinned in docs/requirements.txt. To change them, edit docs/requirements.in, run uv pip compile docs/requirements.in -o docs/requirements.txt, and validate the site again.

Publication

The Documentation workflow builds and checks the site on pushes and pull requests. Only a push to main or a manual run on main can deploy it. Deployment uses GitHub Pages with the GitHub Actions source and a github-pages environment. Pull-request jobs have read-only repository permissions and cannot deploy.

Library revision: fe53ea2f · Lean 4.34.0