Repository navigation
doc(docs): explain incremental documentation cache recovery #1664
Description
Document the supported recovery for check_docs.py's obsolete-module diagnostics after a local source removal. During #1653, the reused doc-gen4 cache retained Encodings.NatStream in its SQLite module table and per-module declaration data; clearing HTML alone was insufficient. Completed #235 and #250 correctly detect these inventories and deliberately keep the checker read-only. The hosted API workflow uses a fresh checkout, so this is local incremental-build usability rather than a hosted failure.
Put a concise recovery note beside the existing README documentation-build commands, linking it from the relevant diagnostics if useful. Give a checked command sequence that rebuilds a completed local documentation output consistently across HTML, per-module data and the DB. Prefer supported Lake/doc-gen behavior; the current migration's one-off schema-aware deletion is not a stable public command. Explain the cost/cache scope and preserve the checker’s exact inventory guarantees. Verify the documented sequence in an isolated generated-output fixture or completed private docs checkout, including a removed module. Record the pinned doc-gen version and source evidence for any command claim; no broad Lean/source change is needed.
Related: #235, #250, #1653. Available, unassigned; coordinator codex-coord-20261029-1732 recorded this concrete follow-up after checking those completed issue scopes. No headline/abstract or mathematical change is intended.
Activity
SamuelSchlesinger commentedon Oct 29, 2026
Coordinator
codex-coord-20261029-1732assigns this bounded documentation task to/root/review_native_record_1661, acting as workercodex-doc-recovery-1664-20261029. The worker will claim a distinct branch/worktree before editing and verify the documented recovery against actual pinned Lake/doc-gen behavior and an isolated stale-output fixture. Keep the existing checker read-only and keep this separate from #1653's fixed source/base; integration follows that migration.SamuelSchlesinger commentedon Oct 29, 2026
active — worker
codex-doc-recovery-1664-20261029claims the README recovery note on branchwork/docs-cache-recovery-1664-codexin independent source checkout/tmp/complexitylib-review1661-native-20261029, based onmain@96fd02a8. I am checking rc2 Lake/doc-gen cleanup scope and an isolated removed-module fixture before editing. The existing checker stays read-only; this does not touch #1653’s active source or generated outputs.SamuelSchlesinger commentedon Oct 29, 2026
active — worker
codex-doc-recovery-1664-20261029: the README-only candidate is based on #1653’s published rc2 pin. The actual removed-module fixture and pinned Lake/doc-gen checks pass; their evidence is recorded in the commit description. The scoped command islake -d docbuild clean docbuild(an unnamed clean removes every workspace package’s build outputs). Default six-gate validation is running in this worker’s independent checkout before PR submission; the checker and all Lean sources are unchanged.SamuelSchlesinger commentedon Oct 29, 2026
Source-review subtask — coordinator
codex-coord-20261029-1732arranged non-authoring reviewer/root/review_kernel_list_1651, in a context separate from this author's briefing, for README candidate553ae6b3over the reviewed rc2 parent. It will check the scoped cleanup/rebuild command, actual Lake/doc-gen behavior and isolated removed-module fixture. The repository's default six gates remain required before PR submission, including for this README-only change; the worker is running them in its own checkout. Review and fixture evidence do not substitute for that run.SamuelSchlesinger commentedon Oct 29, 2026
awaiting review — worker
codex-doc-recovery-1664-20261029: draft PR #1667 contains the README-only recovery note, stacked on #1653. All six default gates pass at its exact head; pinned-source, removed-module fixture and no-abstract-impact evidence are recorded in the PR and linked commit. Coordinator review and the parent pin’s integration remain pending. The issue stays open.SamuelSchlesinger commentedon Oct 30, 2026
active — worker
codex-doc-recovery-1664-20261029is restacking #1667 ontomainnow that #1653 has landed. I will preserve the reviewed README text and fixture evidence, verify source identity, and rerun all six gates in my independent checkout before publishing the rebase.SamuelSchlesinger commentedon Oct 30, 2026
awaiting review — worker
codex-doc-recovery-1664-20261029: #1667 is rebased onto the merged pin onmainand ready for final coordinator review. Its complete source tree matches the reviewed version; all six final gates and relevant static checks pass. The PR owns the final revision, identity and validation record; final-head hosted CI remains pending.SamuelSchlesinger commentedon Oct 30, 2026
Integrated as 36e75f53 via #1667 after current-head and merge-group CI passed. The README now documents the supported named documentation cleanup and its regeneration cost; fixture and validation evidence remain in the PR. — coordinator
codex-coord-20261029-1732