From 3b6219492e3b96c2d0d687b0c1b1961d6d314655 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Thu, 29 Oct 2026 17:35:00 -0400 Subject: [PATCH] doc(docs): explain scoped documentation cache recovery After a removed module leaves obsolete doc-gen inventories, clean only the docbuild package before rebuilding the API docs. HTML, per-module data and the SQLite database must be regenerated together; the named clean retains library/dependency build outputs, package checkouts and Lake artifact cache. Verified with Lean/Lake v4.36.0-rc2 at b35cb10cf2ced51a2fd1880cfdbf75c71ab7a35a and doc-gen4 20afd4ddabd2ef38ffb1a8b930ee0f375e3f75e8. Lake's clean command selects named packages, whose clean method removes only their buildDir: https://github.com/leanprover/lean4/blob/b35cb10cf2ced51a2fd1880cfdbf75c71ab7a35a/src/lake/Lake/CLI/Main.lean#L1175-L1187 https://github.com/leanprover/lean4/blob/b35cb10cf2ced51a2fd1880cfdbf75c71ab7a35a/src/lake/Lake/Config/Package.lean#L431-L433 Doc-gen uses the root package's build directory for doc, doc-data and DB: https://github.com/leanprover/doc-gen4/blob/20afd4ddabd2ef38ffb1a8b930ee0f375e3f75e8/lakefile.lean#L275-L293 https://github.com/leanprover/doc-gen4/blob/20afd4ddabd2ef38ffb1a8b930ee0f375e3f75e8/lakefile.lean#L353-L393 Private fixture: compile Tiny.Current/Tiny.Removed, populate the actual doc-gen SQLite/HTML, then delete Removed and rebuild current modules. Incremental generation retained the obsolete module. Actual scoped Lake clean removed the complete docbuild build directory; repopulation with the same doc-gen binary left only Tiny and Tiny.Current in the DB and HTML. Protected library/dependency outputs, package sources and an isolated LAKE_CACHE_DIR artifact sentinel retained their SHA256 values. Fixture uses direct doc-gen single/fromDb calls matching the inspected Lake facets; it does not assert a full Complexity:docs build in the fixture. Validation: git diff --check and check_docs.py --config-only pass. Default six-gate validation will be recorded on the final supported-pin revision before submitting a PR. No checker code or mathematics changes; curated abstracts, catalogue and PDF renderer have no impact. AI assistance: Codex wrote the README note and performed source/fixture checks. --- README.md | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/README.md b/README.md index f5d647496..b768f75b4 100644 --- a/README.md +++ b/README.md @@ -153,6 +153,20 @@ Open `http://localhost:8000` to browse and search. The **API documentation** wor A manual run on another branch produces an `api-docs` artifact instead; serve it by replacing the directory argument above with the extracted artifact directory. +If removing a source module leaves `check_docs.py` reporting obsolete modules, rebuild the +generated documentation after any documentation build has stopped: + +```bash +lake -d docbuild clean docbuild +lake -d docbuild build Complexity:docs +python3 scripts/check_docs.py +``` + +The named clean removes only `docbuild/.lake/build`, including HTML, per-module data and the +SQLite database; deleting HTML alone leaves stale data behind. Library and dependency build +outputs, package checkouts and Lake's artifact cache are retained. Documentation for all imported +modules is regenerated, which can take substantial time even with warm library build outputs. + #### Checked guide The [guide](guide/ComplexityGuide.lean) introduces the library area by area, with Lean examples