chore: centrally manage released-mirror CI caching

.github/workflows/sync-released.yml

@@ -8,9 +8,10 @@ name: Sync released repos
 # to their `main`, and advances the baseline — one dispatch drives it all the way
 # through. The uncoordinated-commit guard skips any released repo whose `main` has
 # moved off the baseline, so out-of-band commits are never clobbered. Needs the
-# `RELEASED_SYNC_PAT` and `RELEASED_SYNC_PAT_2` secrets (contents:write on the
-# released repos; the set is split across two fine-grained tokens because one
-# token caps its selected-repository list — the sync routes per repo).
+# `RELEASED_SYNC_PAT` and `RELEASED_SYNC_PAT_2` secrets (Contents and Workflows:
+# read/write on the released repos; Workflows is required for managed CI files.
+# The set is split across two fine-grained tokens because one token caps its
+# selected-repository list — the sync routes per repo).
 
 on:
   workflow_dispatch:

AGENTS.md

@@ -44,9 +44,12 @@ near-mechanical copy):
 - `conformance/HexX/{Conformance,EmitFixtures}.lean` — conformance
   drivers (shared `conformance/` sub-project).
 - `conformance-fixtures/HexX/*.jsonl`, `scripts/oracle/<lib>_*.py`.
+- `.github/workflows/ci.yml` — selected from the complete per-repository
+  workflows in `scripts/release/released-ci.yml`.
 
 The publish mechanism is `scripts/release/released.yml` (the per-repo
-managed-path + pin manifest), `scripts/release/sync_released.py` (the
+managed-path + pin manifest), `scripts/release/released-ci.yml` (the managed
+mirror CI workflows), `scripts/release/sync_released.py` (the
 driver; supports `--dry-run`), `scripts/release/synced.json` (the
 per-repo `main` baseline this monorepo corresponds to), and
 `.github/workflows/sync-released.yml` (manual dispatch, dry by default).

PLAN/Releases.md

@@ -178,13 +178,20 @@ In this monorepo, all bench and conformance drivers build in the shared root
 Lake graph. Published mirrors use the corresponding root and sidecar skeletons
 documented in `scripts/release/BOOTSTRAP.md`; the sync manages source and
 rewrites every lockfile but deliberately leaves those Lake skeletons intact.
+The mirrors' CI workflows are managed centrally in
+`scripts/release/released-ci.yml` and published by the same guarded sync.
 
 ### The publish mechanism
 
-Four pieces, under `scripts/release/` and `.github/workflows/`:
+Five pieces, under `scripts/release/` and `.github/workflows/`:
 
 - `released.yml` — a per-repo manifest: which paths to copy, which
   oracles to ship, and which upstream repos to pin, in dependency order.
+- `released-ci.yml` — the complete per-repository mirror workflows. Their
+  repository-specific build, conformance, oracle, and bench commands remain
+  explicit while cache setup and policy are uniform. The explicit cache covers
+  each root/sidecar build plus published Hex dependency builds, while excluding
+  the separately fetched Mathlib cache.
 - `sync_released.py` — the driver. For each repo it clones `main`,
   overwrites the managed paths from this tree, rewrites the cross-repo
   Lake revisions, and commits to `main`. `--dry-run` prints the planned
@@ -212,11 +219,12 @@ routes that repository's clone and push through that token, so a new library
 goes on whichever token has room. Publishing one takes three steps in this
 order:
 
-1. create the repository under `leanprover` and give it the un-managed Lake
-   and CI skeleton (`scripts/release/BOOTSTRAP.md`); the sync clones but never
-   creates;
+1. create the repository under `leanprover`, give it the un-managed Lake
+   skeleton, and add its managed CI workflow in hex-dev
+   (`scripts/release/BOOTSTRAP.md`); the sync clones but never creates;
 2. add that repository to the selected repositories of a token with room,
-   with `Contents: Read and write`, and have an organization owner approve
+   with `Contents: Read and write` and `Workflows: Read and write`, and have an
+   organization owner approve
    the request at
    https://github.com/organizations/leanprover/settings/personal-access-token-requests;
    find the current tokens under
@@ -249,14 +257,13 @@ the push returns `403 Permission to leanprover/<repo>.git denied`.
 before the first push and refuses to start, naming the repositories no token
 covers. A dry run does not preflight, using no token and pushing nothing.
 
-**What the preflight does not prove.** It checks that each repository is in
-some token's selection, and nothing stronger. `GET /repos` needs only
-`Metadata: read`, and the `permissions` it returns describe the authenticated
-user's role rather than that token's grants, so a token holding only
-`Contents: read` on a selected repository still looks fine to it. Nor does it
-know whether branch protection or a ruleset on a mirror's `main` would reject
-the push. Those failures still surface only at push time; the invariant the
-mirrors rely on is that `main` takes direct pushes from the release actor.
+**What the preflight does not prove.** Its receive-pack probe verifies that a
+token can push ordinary content to the selected repository. GitHub checks the
+separate `Workflows: write` permission only when a push changes a workflow, so
+that grant still has to be configured on every publishing token. Nor does the
+probe know whether branch protection or a ruleset on a mirror's `main` would
+reject the push. Those failures still surface only at push time; the invariant
+the mirrors rely on is that `main` takes direct pushes from the release actor.
 
 ### Baseline and the uncoordinated-commit guard
 

scripts/release/BOOTSTRAP.md

@@ -1,11 +1,11 @@
 # Bootstrapping released repositories
 
 `scripts/release/released.yml` is the authoritative publication graph for the
-35 split repositories and the `leanprover/hex` aggregate. The sync workflow
-clones each repository's `main`, overwrites its managed paths from this
-monorepo, copies the release toolchain, synchronizes external dependency locks,
-rewrites every published Hex revision, and pushes the result. It does not
-create repositories or author the remaining Lake and CI skeleton.
+split repositories and the `leanprover/hex` aggregate. The sync workflow
+clones each repository's `main`, overwrites its managed paths and CI workflow
+from this monorepo, copies the release toolchain, synchronizes external
+dependency locks, rewrites every published Hex revision, and pushes the result.
+It does not create repositories or author the remaining Lake skeleton.
 
 The manifest is checked locally by:
 
@@ -60,7 +60,8 @@ on the closest already released package. The initial `main` must contain:
   manifest, with only direct `require`s and the library's declared build
   targets;
 - `lake-manifest.json` generated by Lake, not assembled by hand;
-- `LICENSE`, `AGENTS.md`, `.gitignore`, and the standard single-job CI files;
+- `LICENSE`, `AGENTS.md`, and `.gitignore`; the first sync publishes the
+  repository's workflow from `scripts/release/released-ci.yml`;
 - root and sidecar Lake projects for each enabled `bench` or `conformance`
   directory; and
 - a non-public regression-test `lean_lib` containing every module named by the
@@ -74,12 +75,15 @@ on the closest already released package. The initial `main` must contain:
   root module.
 
 Publication validates these declarations in the unmanaged Lake skeleton before
-copying source. A stale target name therefore stops the sync before it can
-partially update that repository.
+copying source. It also validates that every `scripts/ci` helper named by the
+managed workflow exists in the mirror. A stale target or missing helper
+therefore stops the sync before it can partially update that repository.
 
 Source, the umbrella module, README, SPEC, benchmarks, conformance drivers,
-fixtures, and oracle helpers are managed by the sync when listed in the
-manifest. Do not duplicate or hand-edit those files in a released mirror.
+fixtures, oracle helpers, and `.github/workflows/ci.yml` are managed by the
+sync. Do not duplicate or hand-edit those files in a released mirror. Add a
+new repository's complete workflow to `scripts/release/released-ci.yml`; the
+manifest checker rejects missing and extra workflow entries.
 
 `require`s list direct dependencies only; Lake resolves the rest transitively.
 The longer `pins` list in `released.yml` is deliberate: the sync rewrites the
@@ -112,7 +116,11 @@ Do not add placeholder entries to `scripts/release/synced.json`. An absent
 baseline is how the first publish is distinguished; any truthy, incorrect SHA
 causes the uncoordinated-commit guard to skip the repository.
 
-After every skeleton exists on `main`:
+After every skeleton exists on `main`, ensure the fine-grained tokens behind
+`RELEASED_SYNC_PAT` and
+`RELEASED_SYNC_PAT_2` select every target repository and grant both
+`Contents: Read and write` and `Workflows: Read and write`; the latter is
+required because the sync publishes `.github/workflows/ci.yml`. Then:
 
 1. Run the local manifest check and the complete monorepo build.
 2. Dispatch `.github/workflows/sync-released.yml` with `dry_run=true`.

scripts/release/check_released_manifest.py

@@ -16,7 +16,12 @@
 sys.path.insert(0, str(REPO_ROOT / "scripts"))
 
 from libgraph import load_libraries, reachable_dependencies  # noqa: E402
-from release.sync_released import MANIFEST, managed_paths, removal_paths  # noqa: E402
+from release.sync_released import (  # noqa: E402
+    MANIFEST,
+    managed_paths,
+    released_ci_workflows,
+    removal_paths,
+)
 from release import aggregate_readme  # noqa: E402
 
 
@@ -146,6 +151,147 @@ def release_executables() -> dict[str, str]:
     return out
 
 
+def check_ci_workflows(entries: list[dict]) -> None:
+    """Require one complete, cache-safe managed workflow per released repo."""
+    workflows = released_ci_workflows()
+    expected = {entry["repo"].split("/", 1)[1] for entry in entries}
+    actual = set(workflows)
+    if actual != expected:
+        fail(
+            "released-ci.yml differs from the release manifest; "
+            f"missing={sorted(expected - actual)}, extra={sorted(actual - expected)}"
+        )
+    for entry in entries:
+        short = entry["repo"].split("/", 1)[1]
+        workflow = workflows[short]
+        try:
+            parsed = yaml.load(workflow, Loader=yaml.BaseLoader)
+        except yaml.YAMLError as exc:
+            fail(f"{entry['repo']}: managed CI is invalid YAML: {exc}")
+        triggers = parsed.get("on") if isinstance(parsed, dict) else None
+        push = triggers.get("push") if isinstance(triggers, dict) else None
+        if (
+            not isinstance(push, dict)
+            or push.get("branches") != ["main"]
+            or "pull_request" not in triggers
+        ):
+            fail(
+                f"{entry['repo']}: managed CI must run on main pushes and "
+                "pull requests"
+            )
+        concurrency = parsed.get("concurrency") if isinstance(parsed, dict) else None
+        if (
+            not isinstance(concurrency, dict)
+            or concurrency.get("group") != "${{ github.workflow }}-${{ github.ref }}"
+            or concurrency.get("cancel-in-progress")
+            != "${{ github.ref != 'refs/heads/main' }}"
+        ):
+            fail(
+                f"{entry['repo']}: managed CI must preserve main runs so their "
+                "terminal cache save can finish"
+            )
+        jobs = parsed.get("jobs") if isinstance(parsed, dict) else None
+        if not isinstance(jobs, dict) or not jobs:
+            fail(f"{entry['repo']}: managed CI must define jobs")
+        for job_name, job in jobs.items():
+            if not isinstance(job, dict) or "strategy" in job:
+                fail(f"{entry['repo']}: CI job {job_name} must not use a matrix")
+            steps = job.get("steps") if isinstance(job, dict) else None
+            if not isinstance(steps, list):
+                fail(f"{entry['repo']}: CI job {job_name} has no steps")
+            indexed = {
+                action: [
+                    index for index, step in enumerate(steps)
+                    if isinstance(step, dict) and step.get("uses") == action
+                ]
+                for action in (
+                    "leanprover/lean-action@v1",
+                    "actions/cache/restore@v4",
+                    "actions/cache/save@v4",
+                )
+            }
+            if any(len(indices) != 1 for indices in indexed.values()):
+                fail(
+                    f"{entry['repo']}: CI job {job_name} must contain one "
+                    "lean-action, cache restore, and cache save"
+                )
+            lean_index = indexed["leanprover/lean-action@v1"][0]
+            restore_index = indexed["actions/cache/restore@v4"][0]
+            save_index = indexed["actions/cache/save@v4"][0]
+            if not (lean_index < restore_index < save_index == len(steps) - 1):
+                fail(
+                    f"{entry['repo']}: CI job {job_name} must restore after "
+                    "setup and save only after every verification step"
+                )
+            lean_inputs = steps[lean_index].get("with", {})
+            if lean_inputs.get("use-github-cache") != "false":
+                fail(f"{entry['repo']}: lean-action GitHub cache must be disabled")
+            if lean_inputs.get("use-mathlib-cache") != "false":
+                fail(f"{entry['repo']}: lean-action Mathlib cache must be disabled")
+            restore_inputs = steps[restore_index].get("with", {})
+            save_inputs = steps[save_index].get("with", {})
+            required_paths = {
+                ".lake/build",
+                ".lake/packages/Hex*/.lake/build",
+                ".lake/packages/hex-test-kit/.lake/build",
+            }
+            if job_name == "build" and entry.get("bench"):
+                required_paths |= {
+                    "bench/.lake/build",
+                    "bench/.lake/packages/Hex*/.lake/build",
+                    "bench/.lake/packages/hex-test-kit/.lake/build",
+                }
+            if job_name == "build" and entry.get("conformance"):
+                required_paths |= {
+                    "conformance/.lake/build",
+                    "conformance/.lake/packages/Hex*/.lake/build",
+                    "conformance/.lake/packages/hex-test-kit/.lake/build",
+                }
+            cached_paths = {
+                path.strip()
+                for path in restore_inputs.get("path", "").splitlines()
+                if path.strip()
+            }
+            saved_paths = {
+                path.strip()
+                for path in save_inputs.get("path", "").splitlines()
+                if path.strip()
+            }
+            if cached_paths != required_paths:
+                fail(
+                    f"{entry['repo']}: CI job {job_name} cache paths differ; "
+                    f"missing={sorted(required_paths - cached_paths)}, "
+                    f"extra={sorted(cached_paths - required_paths)}"
+                )
+            key = restore_inputs.get("key", "")
+            restore_prefixes = [
+                prefix.strip()
+                for prefix in restore_inputs.get("restore-keys", "").splitlines()
+                if prefix.strip()
+            ]
+            if (
+                key != save_inputs.get("key")
+                or saved_paths != cached_paths
+                or len(restore_prefixes) != 1
+                or key
+                != restore_prefixes[0]
+                + "${{ github.run_id }}-${{ github.run_attempt }}"
+                or "${{ runner.os }}-${{ runner.arch }}" not in key
+                or "${{ hashFiles(" not in key
+            ):
+                fail(
+                    f"{entry['repo']}: CI job {job_name} cache must use a "
+                    "run-unique save key and stable restore prefix"
+                )
+            save_condition = steps[save_index].get("if", "")
+            if (
+                "github.event_name == 'push'" not in save_condition
+                or "github.ref == 'refs/heads/main'" not in save_condition
+            ):
+                fail(
+                    f"{entry['repo']}: CI job {job_name} must save only from main"
+                )
+
 def main() -> int:
     document = yaml.safe_load(MANIFEST.read_text(encoding="utf-8"))
     entries = document.get("repos") if isinstance(document, dict) else None
@@ -296,6 +442,8 @@ def main() -> int:
 
         seen_repos.add(short)
 
+    check_ci_workflows(entries)
+
     if len(aggregate_entries) != 1:
         fail(f"released.yml must contain exactly one pins_only aggregate; found {len(aggregate_entries)}")
     aggregate = aggregate_entries[0]
@@ -448,7 +596,7 @@ def main() -> int:
 
     print(
         f"release manifest: {len(entries) - 1} split repositories + "
-        f"1 aggregate; paths, pins, test targets, and topological constraints valid"
+        f"1 aggregate; paths, CI, pins, test targets, and topological constraints valid"
     )
     return 0