Publish documentation daily with resumable local analysis

[Vilin97]

Documentation generation currently runs after content pushes and can lose hours of pool analysis at GitHub's six-hour job limit. Move publication to a daily 06:23 UTC workflow with manual dispatch, keeping the existing protected configuration/index preflight on PRs and merge groups.

The publisher pins the Lean 4.35.0-rc3-compatible interproject-linking doc-gen fork, analyzes only LeanPool modules, and links Mathlib and Tau Ceti references to their published docs. Four sequential analysis stages process modules in dependency order with 90-minute allowances, saving integrity-checked SQLite data and Lake markers between stages. A timed-out batch kills its process group and restores the last consistent database/marker pair. A source/pin/policy fingerprint prevents reuse of an obsolete progress cursor; normal Lake traces still validate module reuse.

HTML rendering has a separate job and reads all local records from the database, avoiding an import-all pool environment. Publication requires every local module page, complete same-snapshot analysis, a matching source marker and a validated exposition tree. Existing Pages stays online on failure; an incomplete cold run reports failure and resumes from its checkpoint on the next scheduled/manual run. Checkpoint cleanup uses the existing cache-maintenance workflow. The operations guide documents deployment, recovery and the fork compatibility requirement.

Validation:

• Hosted Python CI: 821 passed, 8 skipped. Fifteen focused import/recovery tests also passed locally, including a real failed-parent/child-writer regression.
• Ruff lint/format, Actionlint and whitespace checks passed.
• Native pinned-Lean/doc-gen smoke tests exercise linked HTML generation, real import all syntax, omission of dependency pages, warm cursor reuse and adding/removing module pages.
• Recovery tests use a real SQLite database and a real subprocess tree to verify rollback and prevention of writes after timeout.

No mathematical sources, Lean validation gates, branch protections or merge-queue requirements are changed. Full-pool publication timing remains to be measured on the first background run.

[greptile-apps]

Advisory cross-file review against Lean Pool's supervisory rubric. This is not by itself a significance, source-verification, or merge verdict.

[High impact] The PR appears safe to merge; both previous findings are fixed and no new blocking issues were found.

Summary

Moves documentation publication to a daily 06:23 UTC run, with manual dispatch.

• Documentation publishes daily while pull requests keep quick preflight checks.
• LeanPool analysis saves verified batches and resumes across runs.
• API pages cover LeanPool modules and link to dependency documentation.

_{Reviews (2) · Last reviewed commit: "Use valid private import-all syntax in t..." · Reviewed by Greptile}

[Vilin97]

Source review of exact head 761e05f6156adb9cf7712a56df45f5d1bad27a29: technically favorable within this eleven-file infrastructure change.

The analysis cursor covers source bytes, dependency pins and link policy. Only completed, database-validated batches advance it; failures restore the SQLite database and Lake markers together after stopping the process group. The import-all parser and failed-parent cleanup fixes are present. Analysis receipts propagate valid skips and reject failed stages or skipped rendering. Rendering requires the complete same-snapshot analysis, every local module page, matching API/exposition source markers and deployment freshness checks.

I also checked removed-module handling against the pinned doc-gen implementation. externals --srcDirs .. deletes missing local modules and their marker/search/backreference/page outputs before fromDb; enabled SQLite foreign keys cascade the corresponding records. Retaining the database across source changes therefore does not leave the suspected stale-module publication path. No extra cleanup implementation is requested. The current Greptile summary's favorable result is consistent with this source assessment, while remaining advisory.

The tests exercise real SQLite rollback, child-process cleanup, cursor invalidation and receipt execution. They were inspected rather than rerun; the owner's full-suite and smoke-test results remain attributed evidence. No independent full-pool documentation timing is claimed.

Integration remains pending a separate policy decision. Current CONTRIBUTING.md says “Never change the checks or gates … unless explicitly asked,” explicitly including workflows and CODE_QUALITY.md. This PR changes both and moves generation away from ordinary pushes; retaining the preflight name does not preserve the former behavior. This review assignment does not supply that separate authorization.

Main 13797a368212c0ae5dca2185a31e1f5338c59821 has only Python CI coverage, with no exact-head Lean or documentation run. The explicit infrastructure hold remains. This comment gives source evidence, not queue admission, auto-merge, approval or merge authorization.