Render complete project APIs with resumable documentation data

[Vilin97]

The fixed LeanPool root imports no projects, so doc-gen4’s library-root renderer publishes only LeanPool.html while omitting independent project API pages. Render the existing docInfo database using every validated public project Imports root plus the core roots, then require nonempty HTML for all 25,363 pool modules in this branch before publication.

The hosted preview exhausted its six-hour job while generating documentation data. A serial preparation job now stops after five hours, stops every database writer, validates and flushes the SQLite checkpoint, and saves it under a unique run/attempt key. The next job must restore that exact checked checkpoint and successfully build the complete LeanPool:docInfo target before rendering, validating all source pages, and uploading the artifact. Actual compiler failures remain failures. Preview artifacts are uploaded without entering the production deployment jobs.

The fixed root, proofs, cards, pinned dependencies and mathematical gates are unchanged. Validation: 725 tests passed, 2 skipped with the required pinned Lean toolchain; Ruff, formatting, Actionlint and diff checks passed. Regression coverage includes an interrupted real SQLite writer, compiler failures, corrupt/empty checkpoints, exact serial cache handoff, and preview artifact scope. The actual repaired renderer, complete artifact coverage and deployed current-main coverage still require hosted verification.

[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 reviewed changes appear safe to merge; no actionable new defect was established.

Summary

The PR renders API pages from every public project root and checks that every pool source has a nonempty page.

• The latest changes split documentation data preparation from the final build, using a time-limited preparation step and an exact cache handoff.
• The final job still requires the full documentation target before rendering or uploading.
• Tests cover interrupted writers, failed builds, invalid checkpoints, and the workflow handoff.
• Hosted rendering and deployed coverage were not verified here. No previous review threads were supplied; GitHub access was unavailable.

_{Reviews (2) · Last reviewed commit: "Preserve bounded documentation preparati..." · Reviewed by Greptile}

[Vilin97]

🤖 LLM review — refactor (gpt-6.1-sol)

Reviewed head: 15013380c54f39d7f147fc138daa81b742812122

Verdict: ✅ approve

The workflow now renders documentation from every validated project Imports root and rejects missing or empty pages for pool sources. It reuses existing index validation and matches the pinned doc-gen4 API. All 29 targeted tests passed. Full-pool rendering and hosted publication were not exercised.

Aspect	Value
Scope	documentation rendering refactor
Introduces tech debt	✅ no
Maintainability	✅ improved
Brittleness	✅ more_robust
Risk	✅ low

The wrapper centralizes coverage checks and preserves renderer failure propagation without introducing an actionable maintenance regression.

---

Tokens: 712,498 in / 6,961 out · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $2.9544 (Standard API equivalent; uncached input) (long-context rate)
Automated review against .github/REFACTOR_REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.

[Vilin97]

Source review of exact 15013380c54f39d7f147fc138daa81b742812122:

The three-file change addresses the fixed root's missing independent-project API pages. structure_errors verifies complete sorted public project Imports roots, and the pinned doc-gen4 fromDb command computes their import closures. Its --manifest option writes an output manifest; this invocation matches the pinned renderer's Lake facet. Publication now requires nonempty HTML for every pool Source, and renderer failure propagates.

The existing Lean builds, proof/quality checks, dependency pins, workflow permissions and deployment-freshness conditions are unchanged. I found no blocking Source defect in this diff.

The actual renderer, generated assets and complete hosted coverage remain unverified: the successful PR checks skipped the documentation-render and deployment jobs. This is a Source assessment, with hosted integration still pending.

Hosted follow-up (2026-10-09): preview run 37948818517, attempt 1 at the same reviewed head was cancelled at 21:07:54 UTC. Documentation-data generation was cancelled; rendering and site validation were skipped. The cancellation reason is unestablished.

The favorable source assessment remains unchanged. Successful pinned rendering, the produced manifest, complete nonempty pool-module pages and generated-asset validation remain pending.

[Vilin97]

Reviewed head f59d1bafacb3aeffbad1c6dc9befd76ed30a2271.

Blocking defect: validate_checkpoint requires a nonempty LeanPool*.doc marker, but the pinned doc-gen4 module facet deliberately writes an empty marker after successfully inserting the module documentation into api-docs.db. The marker is completion evidence; the database contains the documentation. The current test fixture writes artificial nonempty marker content, and test_empty_pool_data_is_not_a_checkpoint currently asserts the opposite of the actual upstream contract.

The current-head full preview 38023512868 failed on October 10. Preparation reached its 18,000-second limit, stopped the build, then raised ValueError: documentation checkpoint has no pool documentation data. Checkpoint identification/cache saving and rendering were skipped. The returned artifact page contains exposition artifacts and no documentation-site.

Required small fix: accept an existing pool completion-marker file without requiring nonzero marker size, while retaining the nonempty database, WAL checkpoint and SQLite integrity checks. Use empty markers in the fixture; verify that a valid database with an empty pool marker succeeds, and that no pool marker or only core/Mathlib markers still fails.

The regular current-head PR checks are green, including pytest, ruff, actionlint and the pool build. They do not establish renderer integration. After the correction, a current-head full preview must complete LeanPool:docInfo, rendering and full-page validation, and upload documentation-site before merge. Generated HTML/assets must remain nonempty. No successful renderer or deployed coverage is claimed.