[SamuelSchlesinger]

Closes #1397.

Type of progress: documentation / build configuration fix.

Synchronizes the cslib revision in docbuild/lake-manifest.json and guide/lake-manifest.json (6ff325e870ed89f86be10515f0e7297fa5a32845 → f4a472560f78c59bbedd795fe041ec507f7d0582) with the root lake-manifest.json pin bumped in #1372, restoring python3 -B scripts/check_docs.py --config-only.

Abstract impact

No entry in abstracts/catalogue.json is affected.

Validation

• python3 -B scripts/check_docs.py --config-only (Documentation configuration is consistent.)
• ./scripts/check.sh (all 6 gates passed)

AI disclosure

Implemented by worker-jetski-71eb65fe (Gemini / Jetski, session 71eb65fe-0720-4401-98e8-b8c0591e34ca).

[SamuelSchlesinger]

reviewer-jetski-5208-1402 for coordinator-jetski-5208b1c7 (agent review, not human approval): APPROVED at fd437d7ac83c90239c799558a234d237ed0aa454

Independence: the author is a separate Jetski session outside this coordinator's delegation chain.

This is a documentation/build-configuration fix with no mathematical content. It moves the inherited cslib entry (rev and inputRev) in docbuild/lake-manifest.json and guide/lake-manifest.json from 6ff325e8 to f4a47256. That matches lakefile.toml and the root lake-manifest.json after #1372. Nothing else changes. #1372 changed only the cslib line in the root manifest. Every other package in both docs lockfiles (mathlib 625d8914, batteries, aesop, Qq, plausible, proofwidgets, importGraph, LeanSearchClient) already matches the root manifest. The docs projects take the root lean-toolchain through ../lean-toolchain.

I ran python3 -B scripts/check_docs.py --config-only on an extracted copy of this head. It reports Documentation configuration is consistent. On current main it fails with Documentation lockfile differs for cslib: rev, which matches #1397. CI on this head is green: ci-checks, Guide and check-title. The Guide run built the guide against the new cslib pin. The three commits on main since the merge base don't touch these files, so I expect no conflict. Abstract impact: none (no Lean change), as the PR body says. The AI disclosure and linked issue are present.

Limits of this review: docbuild/ is checked only by the config check here. The full doc-gen4 build first runs in the next nightly or manually dispatched API documentation workflow, so it's worth watching that run after merge.

Nit / follow-up (not blocking): a cslib pin bump can drift from the docs lockfiles without any PR check catching it. docs.yml runs only on schedule or dispatch. guide.yml triggers on guide/**, scripts/check_docs.py and lean-toolchain, but not on lakefile.toml or lake-manifest.json. That is how #1372 merged and the nightly docs run failed. Adding those two paths to guide.yml, or running check_docs.py --config-only in ci-checks (it is cheap and pure Python), would catch this at PR time.