From 90fb403444596238ad6b1892eb3dd7de290de5da Mon Sep 17 00:00:00 2001 From: Cameron Freer Date: Fri, 4 Sep 2026 12:29:36 +0000 Subject: [PATCH 1/3] ci: cache the docbuild incremental state around API generation MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit doc-gen4's incremental state lives in docbuild/.lake, a separate Lake workspace from the root .lake that lean-action caches, so every master push regenerated the API docs from scratch — nearly the whole of the 45–64 minute master runs against 6–7 minute PR runs. Restore docbuild/.lake/build before `lake build Graphon:docs` and save it immediately after successful generation, keyed by format version, OS, architecture, both toolchains, both manifests, both Lake configurations, and the exact commit, with a dependency-compatible fallback prefix that restores the latest compatible prior state. The save reuses the restore step's primary key and runs only when that key was not already restored. API generation also runs on manual dispatch so the cache can be exercised from a branch; assembly and deployment remain master-only. Add scripts/check_docbuild_sync.py, run right after checkout: the nested workspace must resolve the same toolchain and Mathlib as the root. --- .github/workflows/build.yml | 34 +++++++++++++++- scripts/check_docbuild_sync.py | 74 ++++++++++++++++++++++++++++++++++ 2 files changed, 107 insertions(+), 1 deletion(-) create mode 100644 scripts/check_docbuild_sync.py diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 9d3a76d..c37ad94 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -35,6 +35,11 @@ jobs: - name: Checkout uses: actions/checkout@v7 + # docbuild/ compiles the project's own sources against its own resolved Mathlib; if that + # drifts from the root's, the site build fails while ordinary CI stays green. + - name: Check docbuild sync (toolchain and Mathlib match the root) + run: python3 scripts/check_docbuild_sync.py + - name: Build Lean project and blueprint uses: leanprover/lean-action@c544e89643240c6b398f14a431bcdc6309e36b3e with: @@ -74,12 +79,39 @@ jobs: - name: Build blueprint PDF run: leanblueprint pdf + # doc-gen4's incremental state lives in docbuild/.lake, a separate Lake workspace from the + # root .lake that lean-action caches, so without this it was regenerated from scratch on + # every master push. Restore before generation and save immediately after successful + # generation, so a later TeX, Jekyll, or Pages failure cannot discard a valid cache. The + # build command stays unconditional: the cache supplies prior state, Lake decides freshness. + # Key: format version, OS, arch, both toolchains, both manifests, both Lake configurations, + # and the exact commit; the fallback drops only the commit, restoring the latest compatible + # prior state. Bump docbuild-v1 if the cached path or doc-gen4 layout changes. + # API generation runs on master pushes and on manual dispatch (so the cache can be + # exercised from a branch); assembly and deployment stay master-only below. + - name: Restore docbuild cache + if: (github.ref == 'refs/heads/master' && github.event_name != 'pull_request') || github.event_name == 'workflow_dispatch' + id: docbuild-cache-restore + uses: actions/cache/restore@v4 + with: + path: docbuild/.lake/build + key: docbuild-v1-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'docbuild/lean-toolchain', 'lake-manifest.json', 'docbuild/lake-manifest.json', 'lakefile.toml', 'docbuild/lakefile.toml') }}-${{ github.sha }} + restore-keys: | + docbuild-v1-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'docbuild/lean-toolchain', 'lake-manifest.json', 'docbuild/lake-manifest.json', 'lakefile.toml', 'docbuild/lakefile.toml') }}- + - name: Build API docs - if: github.ref == 'refs/heads/master' && github.event_name != 'pull_request' + if: (github.ref == 'refs/heads/master' && github.event_name != 'pull_request') || github.event_name == 'workflow_dispatch' run: | cd docbuild lake build Graphon:docs + - name: Save docbuild cache + if: ((github.ref == 'refs/heads/master' && github.event_name != 'pull_request') || github.event_name == 'workflow_dispatch') && steps.docbuild-cache-restore.outputs.cache-hit != 'true' + uses: actions/cache/save@v4 + with: + path: docbuild/.lake/build + key: ${{ steps.docbuild-cache-restore.outputs.cache-primary-key }} + - name: Set up Ruby uses: ruby/setup-ruby@v1 with: diff --git a/scripts/check_docbuild_sync.py b/scripts/check_docbuild_sync.py new file mode 100644 index 0000000..278c8a5 --- /dev/null +++ b/scripts/check_docbuild_sync.py @@ -0,0 +1,74 @@ +#!/usr/bin/env python3 +"""Guard: the docbuild sub-project must resolve the same toolchain and Mathlib as the root. + +`docbuild/` depends on `../`, so it compiles the project's own sources. If it resolves a +different Mathlib, the site build compiles current sources against a stale Mathlib and fails +on names that do not exist there yet — while ordinary CI stays green, because ordinary CI +never enters `docbuild/`. + +That has happened twice across toolchain bumps, so it is checked rather than remembered. + +Note on the nested `docbuild/lean-toolchain`: it cannot simply be deleted. `lake update` +regenerates it from the resolved dependency graph, and does so with the correct value. The +stale toolchain and the stale manifest were never two mistakes — both are what a *missing* +`cd docbuild && lake update` looks like. So this guard compares rather than forbids, and the +remedy for every failure below is the same single command. + +Run with: python3 scripts/check_docbuild_sync.py +""" + +import json +import pathlib +import sys + +ROOT = pathlib.Path(__file__).resolve().parent.parent +REMEDY = "Regenerate with: cd docbuild && lake update" + + +def revs(manifest: pathlib.Path) -> dict[str, str]: + data = json.loads(manifest.read_text()) + return {p["name"].strip("«»"): p.get("rev") for p in data["packages"]} + + +def main() -> int: + root_manifest = ROOT / "lake-manifest.json" + docbuild_manifest = ROOT / "docbuild" / "lake-manifest.json" + root_toolchain = ROOT / "lean-toolchain" + docbuild_toolchain = ROOT / "docbuild" / "lean-toolchain" + + for f in (root_manifest, docbuild_manifest, root_toolchain, docbuild_toolchain): + if not f.exists(): + print(f"FAIL: {f.relative_to(ROOT)} is missing") + print(REMEDY) + return 1 + + failures = [] + + rt = root_toolchain.read_text().strip() + dt = docbuild_toolchain.read_text().strip() + if rt != dt: + failures.append(f" toolchain: root {rt!r} vs docbuild {dt!r}") + + root_revs, doc_revs = revs(root_manifest), revs(docbuild_manifest) + for name, root_rev in root_revs.items(): + doc_rev = doc_revs.get(name) + if doc_rev is None: + failures.append(f" {name}: absent from docbuild manifest (root {root_rev})") + elif doc_rev != root_rev: + failures.append(f" {name}: root {root_rev} vs docbuild {doc_rev}") + + if failures: + print("FAIL: docbuild is out of sync with the root project:") + print("\n".join(failures)) + print(REMEDY) + return 1 + + print( + f"OK: docbuild matches the root project — toolchain {rt}, " + f"{len(root_revs)} shared packages, Mathlib {root_revs.get('mathlib')}." + ) + return 0 + + +if __name__ == "__main__": + sys.exit(main()) From 8137c5be8bf96a541728eb0d275943d2b812e5e5 Mon Sep 17 00:00:00 2001 From: Cameron Freer Date: Sun, 6 Sep 2026 08:43:39 +0000 Subject: [PATCH 2/3] ci: empty commit to exercise the SHA-free docbuild cache fallback From 4e3b9cf38ead70ee08c0946ba57ea7b8c0cbe367 Mon Sep 17 00:00:00 2001 From: Cameron Freer Date: Sun, 6 Sep 2026 10:07:57 +0000 Subject: [PATCH 3/3] ci: restore the docbuild cache before lean-action Retrieve the small docs entry, refreshing its last-access time, before this run adds another large root cache; eviction is by last access under the repository limit. Saving stays immediately after successful API generation. --- .github/workflows/build.yml | 43 ++++++++++++++++++++----------------- 1 file changed, 23 insertions(+), 20 deletions(-) diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index c37ad94..0ed5804 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -40,6 +40,29 @@ jobs: - name: Check docbuild sync (toolchain and Mathlib match the root) run: python3 scripts/check_docbuild_sync.py + # doc-gen4's incremental state lives in docbuild/.lake, a separate Lake workspace from the + # root .lake that lean-action caches, so without this it was regenerated from scratch on + # every master push. Restore it here, before lean-action saves this run's large root + # cache, so the small docs entry is retrieved and its last-access refreshed before more + # storage pressure is added (eviction is by last access); save immediately after successful + # generation, so a later TeX, Jekyll, or Pages failure cannot discard a valid cache. The + # build command stays unconditional: the cache supplies prior state, Lake decides freshness. + # Key: format version, OS, arch, both toolchains, both manifests, both Lake configurations, + # and the exact commit; the fallback drops only the commit, restoring the latest compatible + # prior state. Bump docbuild-v1 if the cached path or doc-gen4 layout changes. + # API generation runs on master pushes and on manual dispatch (so the cache can be + # exercised from a branch); assembly and deployment stay master-only below. + - name: Restore docbuild cache + if: (github.ref == 'refs/heads/master' && github.event_name != 'pull_request') || github.event_name == 'workflow_dispatch' + id: docbuild-cache-restore + uses: actions/cache/restore@v4 + with: + path: docbuild/.lake/build + key: docbuild-v1-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'docbuild/lean-toolchain', 'lake-manifest.json', 'docbuild/lake-manifest.json', 'lakefile.toml', 'docbuild/lakefile.toml') }}-${{ github.sha }} + restore-keys: | + docbuild-v1-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'docbuild/lean-toolchain', 'lake-manifest.json', 'docbuild/lake-manifest.json', 'lakefile.toml', 'docbuild/lakefile.toml') }}- + + - name: Build Lean project and blueprint uses: leanprover/lean-action@c544e89643240c6b398f14a431bcdc6309e36b3e with: @@ -79,26 +102,6 @@ jobs: - name: Build blueprint PDF run: leanblueprint pdf - # doc-gen4's incremental state lives in docbuild/.lake, a separate Lake workspace from the - # root .lake that lean-action caches, so without this it was regenerated from scratch on - # every master push. Restore before generation and save immediately after successful - # generation, so a later TeX, Jekyll, or Pages failure cannot discard a valid cache. The - # build command stays unconditional: the cache supplies prior state, Lake decides freshness. - # Key: format version, OS, arch, both toolchains, both manifests, both Lake configurations, - # and the exact commit; the fallback drops only the commit, restoring the latest compatible - # prior state. Bump docbuild-v1 if the cached path or doc-gen4 layout changes. - # API generation runs on master pushes and on manual dispatch (so the cache can be - # exercised from a branch); assembly and deployment stay master-only below. - - name: Restore docbuild cache - if: (github.ref == 'refs/heads/master' && github.event_name != 'pull_request') || github.event_name == 'workflow_dispatch' - id: docbuild-cache-restore - uses: actions/cache/restore@v4 - with: - path: docbuild/.lake/build - key: docbuild-v1-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'docbuild/lean-toolchain', 'lake-manifest.json', 'docbuild/lake-manifest.json', 'lakefile.toml', 'docbuild/lakefile.toml') }}-${{ github.sha }} - restore-keys: | - docbuild-v1-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'docbuild/lean-toolchain', 'lake-manifest.json', 'docbuild/lake-manifest.json', 'lakefile.toml', 'docbuild/lakefile.toml') }}- - - name: Build API docs if: (github.ref == 'refs/heads/master' && github.event_name != 'pull_request') || github.event_name == 'workflow_dispatch' run: |