# 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:

```sh
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:

```sh
lake exe cache get
lake build
```

Then build the API using the committed documentation manifest:

```sh
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:

```sh
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.