csd-lean4-docs

Build-and-publish project for the csd-lean4 API documentation.

The rendered docs: https://docs.constraintsurfacedynamics.com

There is nothing here but a lakefile.toml and a workflow. No Lean source, no committed HTML.

Why this repo exists

A GitHub repository gets one Pages site, and csd-lean4's is already spent: its glossary.yml publishes the CSD glossary to glossary.constraintsurfacedynamics.com. A second Pages deploy in the same repository would collide with it, and two workflows publishing one artefact would race.

Mathlib hit the same constraint and solved it this way — leanprover-community/mathlib4_docs is a thin repo that checks out the corpus beside itself, builds the docs, and hands them to Pages. This is that pattern, pointed at csd-lean4.

The built output is never committed. A doc-gen4 render of a corpus this size would bloat git history permanently, and committed HTML is exactly what lets a site and its source disagree.

Two differences from Mathlib's setup, both deliberate

doc-gen4 is pinned to the Lean toolchain tag, not main. csd-lean4 is not tracking Mathlib nightly, so the conservative pin is the right one. It is the pin csd-lean4's own docs.yml already uses. CI rewrites the rev line in lakefile.toml from the corpus's lean-toolchain on every run, so the committed value cannot silently drift.

A custom domain. Mathlib serves at the default leanprover-community.github.io/mathlib4_docs/ and takes no custom domain — which costs them nothing, because that host is their institutional identity. zblore.github.io is not CSD's, and these docs would otherwise be the only CSD surface outside the programme's domain. Hence CNAME, and a DNS record, following the precedent the glossary set.

The name is docs., not api.: csd-lean4 is a formalisation corpus, not a library with a public interface, and calling it an API would overclaim.

Building locally

The corpus is required by relative path, so the two repos must sit side by side with these exact directory names:

some-parent/
  csd-lean4/
  csd-lean4-docs/

Then:

cd csd-lean4 && lake exe cache get && lake build CsdLean4
cd ../csd-lean4-docs
cp ../csd-lean4/lean-toolchain .
echo "-- docbuild scratch root" > Docbuild.lean
lake update doc-gen4
lake build CsdLean4:docs
# output in .lake/build/doc

lean-toolchain and Docbuild.lean are gitignored: CI materialises both from the corpus, so that the toolchain is pinned in exactly one place.

What guards what

This repo publishes. csd-lean4's own .github/workflows/docs.yml guards — it runs doc-gen4 as a smoke test and checks that named declarations still render, as part of that repo's hygiene. It is not superseded by this one and should not be deleted.