[Vilin97]

Follow-up to #759.

Problem

The DocsState checkpoint key hashed lakefile.toml together with the toolchain and manifest pins, and its only restore key kept that same hash. Every lakefile.toml edit therefore threw away all saved docInfo. With 31,178 pool modules, a cold analysis needs more than one daily run (about 24k modules fit in the four 90-minute stages), so a lakefile edit delays the next deploy by at least a day. lakefile.toml has changed 11 times since September, including #712 and #751 today.

Change

• Move lakefile.toml into its own key segment: DocsState-v1-<os>-<toolchain+manifest+docbuild>-<lakefile>-<run>-<attempt>-<stage>.
• Restore keys: first the exact lakefile hash (same behavior as before), then a fallback with any lakefile hash.
• Add a contract test that the fallback still pins the toolchain and manifest but not the root lakefile.toml.

Why it's safe

• Lake checks every restored docInfo trace and rebuilds the ones whose inputs changed. For example, the Fix proof-length counter including unrelated declarations #712 plugin and Make every Lean warning a compile error (warningAsError, like Tau Ceti) #751 warningAsError changes still rebuild every pool module, as they should.
• input_identity still hashes lakefile.toml, so a fallback restore resets the analysis cursor and the render gate still requires a full pass over the current snapshot.
• Toolchain, Mathlib, or doc-gen pin changes still start from a clean checkpoint, as before.
• No check or gate changes.

The gain is for lakefile edits that leave build traces alone, such as adding an executable, changing globs, or retiring a library. Four of the last 11 edits were like that.

Testing

• uv run --group test pytest tests/test_ci_cache_contract.py tests/test_documentation.py: 97 passed. test_native_build_failure_stops_child_writers[True] failed once and then passed on 3 reruns; it's flaky and this change doesn't touch it.
• ruff check, ruff format --check, and actionlint pass.

🤖 Generated with Claude Code

[github-actions]

Proof profile (new / modified Lean files)

No added or modified Lean files under LeanPool/ in this PR. No compile-cost measurements are needed.

Advisory only — never blocks merge.

[Vilin97]

User authorization for this workflow change is recorded for the permanent reviewer in Vilin97/lean-pool-automation#14 (merged as e65f8fa2e).

[greptile-apps]

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

[Medium impact] The PR appears safe to merge; no actionable issue was found.

Summary

Separates the root lakefile.toml hash from the pinned documentation inputs in DocsState keys.

• Documentation runs can reuse checkpoints after pool lakefile edits.

Vilin97 explicitly describes resetting the analysis cursor after a fallback restore as intentional. Saved build results remain available for Lake to check again.

_{Reviews (1) · Last reviewed commit: "fix(docs): reuse documentation checkpoin..." · Reviewed by Greptile}

[Vilin97]

{
"summary": "Technical source review at 89f3c8a: split the pool lakefile hash into a separate documentation-checkpoint key segment, trying the same configuration before a broader fallback. The cursor still hashes the lakefile, rejects stale completion and revisits every current module through Lake's trace checks. Two cache-contract tests and a real-consumer cursor-reset probe passed. The first rollout can still miss old-format caches; no hosted recovery or performance gain is established. Direct scoped workflow authorization is verified; current-head CI and normal protected integration remain separate.",
"assessment": {
"scope": "Documentation checkpoint cache-key fallback and contract test",
"introduces_tech_debt": false,
"maintainability": "improved",
"brittleness": "unchanged",
"risk": "low",
"assessment_one_sentence": "Allows more checkpoint reuse while retaining current-input, dependency-pin, trace and full-completion validation."
},
"verdict": "approve",
"findings": []
}