Context
The Documentation workflow can become very slow after Lean/Mathlib/doc-gen bumps. In the v4.32 bump, the docs job completed but took over 5 hours:
A PR doc run that started before that cache save restored the old docs cache instead, so it kept rebuilding from the stale v4.31-era doc cache even though the new main run eventually warmed the v4.32 cache.
Why this happens
lake build LeanPool benefits from Mathlib oleans via lake exe cache get, but cd docbuild && lake build LeanPool:docs has extra doc-gen work. The doc-gen4 docInfo facet recursively materializes documentation metadata for imported modules and writes a SQLite docs database, then renders HTML/search data. On a cold dependency bump, this includes thousands of modules from Mathlib and other dependencies, not just LeanPool files.
The docs cache is currently saved only on main, and PRs restore by prefix. This means a PR started while main is still building docs cannot use the cache that main will save later.
TODO
Notes
The current cold build duration is close enough to the 6-hour GitHub-hosted runner ceiling that future repository growth or a slower runner could turn this into a hard timeout.
Context
The
Documentationworkflow can become very slow after Lean/Mathlib/doc-gen bumps. In the v4.32 bump, the docs job completed but took over 5 hours:Build documentationstep ran from2026-06-23T21:56:20Zto2026-06-24T02:59:41Z.2026-06-24T03:02:20Z.A PR doc run that started before that cache save restored the old docs cache instead, so it kept rebuilding from the stale v4.31-era doc cache even though the new main run eventually warmed the v4.32 cache.
Why this happens
lake build LeanPoolbenefits from Mathlib oleans vialake exe cache get, butcd docbuild && lake build LeanPool:docshas extra doc-gen work. Thedoc-gen4docInfofacet recursively materializes documentation metadata for imported modules and writes a SQLite docs database, then renders HTML/search data. On a cold dependency bump, this includes thousands of modules from Mathlib and other dependencies, not just LeanPool files.The docs cache is currently saved only on
main, and PRs restore by prefix. This means a PR started whilemainis still building docs cannot use the cache thatmainwill save later.TODO
.github/workflows/docs.yml, preferring same toolchain/manifest/doc-gen dependency hashes before falling back to broadDocs-Lake-${{ runner.os }}-caches.LeanPool.leanfrom the dependency-level restore prefix so content PRs reuse same-version doc caches more predictably.main/manual dispatch. Lean CI already checks build, lint, style, and repository quality.LeanPool.*modules while linking Mathlib/dependency declarations to external documentation, instead of rebuilding dependency doc pages locally.timeout-minutesfor the docs job so cold builds fail predictably before the GitHub-hosted runner limit.maindocs cache is saved, cancel/rerun PR docs jobs that started before the cache was warm.Notes
The current cold build duration is close enough to the 6-hour GitHub-hosted runner ceiling that future repository growth or a slower runner could turn this into a hard timeout.