Fix documentation cache bootstrap

[Vilin97]

Root cause

The documentation workflow restored an OS-only Docs-Lake-* fallback after the Lean 4.33 bump. That pulled Lean 4.32 artifacts, and the directory-only Mathlib check then skipped lake exe cache get. The job spent most of its six-hour limit rebuilding stale artifacts and timed out before it could save a compatible cache, creating a bootstrap deadlock.

Fix

• restore the core Lake-* cache with the same key, paths, and ordering as Lean Action CI
• install the Mathlib cache unconditionally and verify its manifest revision
• split Mathlib docInfo into a bounded job and hand off a WAL-checkpointed, integrity-checked SQLite cache
• keep doc-gen state in compatibility-scoped caches containing only doc output and five doc-only dependencies
• checkpoint pool docInfo before rerendering HTML; never cache duplicate root artifacts or HTML
• fail cheaply on root/docbuild toolchain, Mathlib, and generated-root divergence
• let cold main bootstraps finish while suppressing superseded deployments using workflow-run freshness checks
• apply the same root-cache repair to Exposition Verify

Validation

• actionlint -color
• git diff --check
• local root/docbuild compatibility assertions
• local lake exe mk_all --check
• three independent read-only workflow/cache reviews
• PR CI exercises the new cold-cache producer/consumer handoff

[greptile-apps]

Greptile Summary

This PR fixes a cache bootstrap deadlock introduced by the Lean 4.33 toolchain bump: the old Docs-Lake-* fallback restored Lean 4.32 artifacts, the directory check skipped lake exe cache get, and the doc job exhausted its six-hour limit without ever saving a compatible cache.

• Cache namespace split: a new preflight job validates toolchain/Mathlib consistency and gates a dedicated mathlib_doc_info job that builds Mathlib:docInfo, WAL-checkpoints and integrity-checks the SQLite output, and saves a DocsInfoMathlib-v3-* checkpoint; build then tries its own DocsInfo-v3-* pool checkpoint first and falls back to the Mathlib-only one with fail-on-cache-miss: true, preventing silent cold-start failures.
• Root cache alignment: all jobs now restore the same Lake-* key/paths as Lean Action CI, eliminating the stale-artifact fallback; Mathlib install is unconditional and verified against lake-manifest.json in every job.
• Deployment guard: a new deployment_freshness job compares GITHUB_RUN_NUMBER against the latest main run via the GitHub API to suppress stale deployments; a second inline recheck in deploy narrows the race window just before actions/deploy-pages; cancel-in-progress is now false on main so cold bootstrap runs can seed new caches without being preempted.

Confidence Score: 5/5

Safe to merge — all job dependency edges, cache key namespaces, SQLite WAL validation, and freshness guards are logically consistent; no existing deploy path is left unprotected.

The cache bootstrap is well-structured: the mathlib_doc_info to build handoff is enforced by an explicit needs dependency, fail-on-cache-miss prevents silent cold-start failures, and WAL checkpoint plus integrity checks run before any save. The freshness gate is defended at two points. The concurrency change correctly queues rather than cancels main runs. No correctness gap was found in the critical path.

Files Needing Attention: No files require special attention beyond the minor self-referential hardcoded filename noted in the review comment.

Important Files Changed

Filename	Overview
.github/workflows/docs.yml	Major restructure: adds preflight, mathlib_doc_info, and deployment_freshness jobs; splits cache namespaces; migrates to Lake-* keys matching Lean Action CI; introduces conditional doc-checkpoint restore with fail-on-cache-miss guard and per-job SQLite WAL validation
.github/workflows/exposition-verify.yml	Parallel fix: replaces Docs-Lake-* cache key with Lake-* to match Lean Action CI; removes docbuild from paths; unconditional Mathlib install with manifest-revision verification

Flowchart

%%{init: {'theme': 'neutral'}}%%
flowchart TD
    A[preflight\nToolchain + Mathlib compatibility\nCache restore + mk_all check] --> B[mathlib_doc_info\nBuild Mathlib:docInfo\nWAL checkpoint + save DocsInfoMathlib-v3-*]
    A --> C[exposition\nBuild LeanPool + extract\nGenerate Python site]
    B --> C
    B --> D[build\nRestore DocsInfo-v3-* pool checkpoint\nFallback: DocsInfoMathlib-v3- fail-on-miss\nBuild LeanPool:docInfo + docs\nWAL checkpoint + save DocsInfo-v3-*]
    A --> D
    C --> E[deployment_freshness\nCompare run_number vs latest main run\nOutput: deploy=true/false]
    D --> E
    E --> F[deploy\nif: deploy==true\nAssemble site\nRecheck freshness\nDeploy Pages]
    C --> F
    D --> F

Loading

_{Reviews (2): Last reviewed commit: "Harden documentation preflight diagnosti..." | Re-trigger Greptile}