diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 9d3a76d..0ed5804 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -35,6 +35,34 @@ 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 + + # 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: @@ -75,11 +103,18 @@ jobs: run: leanblueprint pdf - 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())