From c8a361166082d3c82044418abe6aace46da169bf Mon Sep 17 00:00:00 2001
From: Eduardo Gomes <eduardogbg@gmail.com>
Date: Thu, 11 Jun 2026 16:16:33 -0300
Subject: [PATCH 1/8] docker: bake the mathlib ltar store into the CI image

Ship only the ~0.4GB ltar store at /opt/mathlib-cache:
bake_mathlib_cache.sh fills it from mathlib's cloud cache when it still
serves the pinned rev, else from a full source build plus
'lake exe cache pack', and fails the image build on an incomplete store.
The image tag gains the mathlib rev and a hash of the docker build
context, so editing the recipe or any COPY'd file retags the image.
---
 docker/ci/Dockerfile                  | 45 ++++++++++++++++++++++++
 docker/ci/bake_mathlib_cache.sh       | 38 +++++++++++++++++++++
 scripts/ci/read_toolchain_versions.py | 49 +++++++++++++++++++++++++++
 3 files changed, 132 insertions(+)
 create mode 100755 docker/ci/bake_mathlib_cache.sh

diff --git a/docker/ci/Dockerfile b/docker/ci/Dockerfile
index 25b8f70e..8cb90d1e 100644
--- a/docker/ci/Dockerfile
+++ b/docker/ci/Dockerfile
@@ -52,3 +52,48 @@ RUN if [ -n "$NOIR_REV" ]; then \
         cp /opt/noir/target/release/nargo /usr/local/bin/nargo; \
         rm -rf /opt/noir/.git /opt/noir/target; \
     fi
+
+# Bake mathlib's `.ltar` store into the image so CI jobs depend on neither
+# mathlib's cloud olean cache nor GitHub-cache round-trips. Only the store
+# (~0.4GB) ships in the image: a fully built dependency tree unpacks to ~8GB
+# more, and GitHub's hosted runners guarantee only ~14GB free while
+# container-job image pulls happen before any job step can free disk, so a
+# tree-carrying image makes every pull a coin flip against the runner's free
+# space. CI jobs instead clone the dependency sources into a host-side shared
+# dir and `lake exe cache get` decompresses offline from this store.
+#
+# bake_mathlib_cache.sh populates the store at image-build time, cheapest
+# source first:
+#   1. `lake exe cache get-` (download only, no decompression) in the bake
+#      workspace, when mathlib's cloud cache still serves the pinned rev.
+#   2. Full source build + `lake exe cache pack` from the built tree.
+# The bake workspace reuses Lampe's lakefile and manifest so the packed
+# revisions always match the pin; lake needs only the config files (not the
+# Lampe sources) to materialize and build dependency targets. Each step is
+# gated on the store still being too small to be a complete mathlib cache
+# (mathlib is ~7k modules, one `.ltar` per module).
+#
+# `cache pack` must run with the mathlib clone as the workspace root and with
+# the dependency clones physically inside mathlib's own `.lake/packages`,
+# mirroring mathlib's CI: `.ltar` archives store workspace-root-relative
+# paths (`.lake/build/...` for mathlib itself, `.lake/packages/<dep>/...`
+# for dependencies), and `cache get` in downstream workspaces relies on
+# exactly that layout (it redirects mathlib's own modules to the package dir
+# at decompression time and dependency modules resolve to the same relative
+# paths). Packing from a downstream root, or with the dependencies behind a
+# symlink, bakes wrong (downstream-prefixed or absolute) paths into the
+# archives. The script therefore moves the dependencies under the mathlib
+# root for the pack; mathlib's manifest pins exactly the revisions Lampe
+# inherits, so lake accepts them as-is.
+#
+# Everything except the store is transient: the clones and build artifacts
+# are deleted in the same RUN that created them, so they never reach a
+# layer. An image with a missing or partial store would silently push every
+# CI job back onto mathlib's cloud cache or a full source build, so the bake
+# fails instead of shipping one.
+ENV MATHLIB_CACHE_DIR=/opt/mathlib-cache
+
+COPY Lampe/lean-toolchain Lampe/lakefile.lean Lampe/lake-manifest.json \
+    docker/ci/bake_mathlib_cache.sh /opt/lake-bake/
+
+RUN /opt/lake-bake/bake_mathlib_cache.sh
diff --git a/docker/ci/bake_mathlib_cache.sh b/docker/ci/bake_mathlib_cache.sh
new file mode 100755
index 00000000..ba10839f
--- /dev/null
+++ b/docker/ci/bake_mathlib_cache.sh
@@ -0,0 +1,38 @@
+#!/usr/bin/env bash
+# Populates the mathlib `.ltar` store at $MATHLIB_CACHE_DIR from the bake
+# workspace at /opt/lake-bake. See the comment block in docker/ci/Dockerfile
+# for why the store is baked into the image and how the layout works.
+set -euo pipefail
+
+store_ltars() {
+  find "${MATHLIB_CACHE_DIR}" -type f -name '*.ltar' | wc -l
+}
+
+mkdir -p "${MATHLIB_CACHE_DIR}"
+cd /opt/lake-bake
+
+if [ "$(store_ltars)" -lt 1000 ]; then
+  lake exe cache get- || true
+fi
+
+if [ "$(store_ltars)" -lt 1000 ]; then
+  lake exe cache get || true
+  lake build mathlib/Mathlib batteries/Batteries
+  cd .lake/packages/mathlib
+  mkdir -p .lake/packages
+  for dep in /opt/lake-bake/.lake/packages/*/; do
+    dep=${dep%/}
+    if [ "$(basename "$dep")" != mathlib ]; then
+      mv "$dep" .lake/packages/
+    fi
+  done
+  lake exe cache pack
+  cd /opt/lake-bake
+fi
+
+rm -rf /opt/lake-bake/.lake
+
+if [ "$(store_ltars)" -lt 1000 ]; then
+  echo "mathlib ltar store is incomplete ($(store_ltars) archives); refusing to ship it"
+  exit 1
+fi
diff --git a/scripts/ci/read_toolchain_versions.py b/scripts/ci/read_toolchain_versions.py
index c8194e93..af86fac1 100644
--- a/scripts/ci/read_toolchain_versions.py
+++ b/scripts/ci/read_toolchain_versions.py
@@ -1,4 +1,6 @@
 #!/usr/bin/env python3
+import hashlib
+import json
 import os
 import pathlib
 import re
@@ -39,6 +41,47 @@ def read_noir_rev(root: pathlib.Path) -> str:
     return cargo["dependencies"]["noirc_driver"]["rev"]
 
 
+def read_mathlib_rev_from(manifest_path: pathlib.Path) -> str:
+    manifest = json.loads(manifest_path.read_text())
+    for package in manifest["packages"]:
+        if package["name"] == "mathlib":
+            return package["rev"]
+    raise SystemExit(f"mathlib package not found in {manifest_path}")
+
+
+def read_mathlib_rev(root: pathlib.Path) -> str:
+    lampe_rev = read_mathlib_rev_from(root / "Lampe" / "lake-manifest.json")
+    stdlib_rev = read_mathlib_rev_from(root / "stdlib" / "lampe" / "lake-manifest.json")
+    if stdlib_rev != lampe_rev:
+        raise SystemExit(
+            "Lampe and stdlib mathlib revisions differ; update them together."
+        )
+    return lampe_rev
+
+
+def read_docker_context_hash(root: pathlib.Path) -> str:
+    # The tag must change whenever the image recipe changes, otherwise the
+    # existence check in build-ci-image keeps serving the old image forever.
+    # The hash covers every file the Dockerfile COPYs into the image plus the
+    # recipe itself: the whole docker/ci/ directory and the COPY'd repo files.
+    paths = [
+        path
+        for path in (root / "docker" / "ci").rglob("*")
+        if path.is_file()
+    ]
+    paths += [
+        root / "scripts" / "requirements.txt",
+        root / "Lampe" / "lakefile.lean",
+        root / "Lampe" / "lake-manifest.json",
+    ]
+    paths.sort()
+    digest = hashlib.sha256()
+    for path in paths:
+        digest.update(path.relative_to(root).as_posix().encode())
+        digest.update(path.read_bytes())
+    return digest.hexdigest()[:8]
+
+
 def write_output(key: str, value: str) -> None:
     output_path = os.environ.get("GITHUB_OUTPUT")
     if output_path:
@@ -53,18 +96,24 @@ def main() -> None:
     rust_stable = read_rust_stable(root)
     lean_toolchain = read_lean_toolchain(root)
     noir_rev = read_noir_rev(root)
+    mathlib_rev = read_mathlib_rev(root)
 
     lean_tag = lean_version_for_tag(lean_toolchain)
     noir_short = normalize_tag(noir_rev)[:4]
+    mathlib_short = normalize_tag(mathlib_rev)[:8]
+    context_short = read_docker_context_hash(root)
     image_tag = (
         f"rust-{normalize_tag(rust_stable)}"
         f"-lean-{lean_tag}"
         f"-noir-{noir_short}"
+        f"-mathlib-{mathlib_short}"
+        f"-ctx-{context_short}"
     )
 
     write_output("rust_stable", rust_stable)
     write_output("lean_toolchain", lean_toolchain)
     write_output("noir_rev", noir_rev)
+    write_output("mathlib_rev", mathlib_rev)
     write_output("image_tag", image_tag)
 
 

From 917e97c6605a3eaeb8b28c79147a1c5c3aebda78 Mon Sep 17 00:00:00 2001
From: Eduardo Gomes <eduardogbg@gmail.com>
Date: Thu, 11 Jun 2026 16:16:33 -0300
Subject: [PATCH 2/8] ci: free disk space on both host and container runners

Container jobs clear the bind-mounted /__t; host runners drop
/opt/hostedtoolcache, the Android SDK, and the .NET tree.
---
 .github/actions/free-disk-space/action.yml | 23 +++++++++++++---------
 1 file changed, 14 insertions(+), 9 deletions(-)

diff --git a/.github/actions/free-disk-space/action.yml b/.github/actions/free-disk-space/action.yml
index c3f8a754..f935e437 100644
--- a/.github/actions/free-disk-space/action.yml
+++ b/.github/actions/free-disk-space/action.yml
@@ -1,20 +1,25 @@
 name: 'Free Runner Disk Space'
 description: >-
-  Drop the bind-mounted /opt/hostedtoolcache before heavy lake/mathlib
-  steps. GH-hosted Ubuntu runners preinstall ~14 GB of language
-  toolchains (Python/Node/Ruby/Go/Java/.NET) under that path, which the
-  container sees as /__t. Our jobs never use any of it, but
-  `lake exe cache get` decompresses ~8 k mathlib oleans into the same
-  disk and the combined peak occasionally exceeds the runner disk
+  Drop the preinstalled toolchain bloat before heavy lake/mathlib or
+  docker-build steps. GH-hosted Ubuntu runners preinstall ~14 GB of language
+  toolchains (Python/Node/Ruby/Go/Java/.NET) under /opt/hostedtoolcache,
+  which container jobs see bind-mounted as /__t. Our jobs never use any of
+  it, but `lake exe cache get` decompresses ~8 k mathlib oleans into the
+  same disk and the combined peak occasionally exceeds the runner disk
   limit, manifesting as `No space left on device` mid-decompression.
-  Drop the tool cache proactively to give decompression headroom.
+  Inside a container the action clears /__t; on the host it removes the
+  tool cache plus the Android SDK and .NET trees.
 runs:
   using: 'composite'
   steps:
-    - name: Free /opt/hostedtoolcache
+    - name: Free Preinstalled Toolchains
       shell: bash
       run: |
         set -eu
         df -h /
-        rm -rf /__t/*
+        if [ -d /__t ]; then
+          rm -rf /__t/*
+        else
+          sudo rm -rf /opt/hostedtoolcache /usr/local/lib/android /usr/share/dotnet
+        fi
         df -h /

From 8316fd036902aba785f69d0ca77425355baa4e80 Mon Sep 17 00:00:00 2001
From: Eduardo Gomes <eduardogbg@gmail.com>
Date: Thu, 11 Jun 2026 16:16:33 -0300
Subject: [PATCH 3/8] ci: split build-ci-image into check, build, and guard
 jobs

check probes GHCR for the tag with 'docker manifest inspect' (replacing
verify_ci_image.py), build runs under a single job-level condition
(image missing and pushes allowed), and guard fails fork PRs whose
image is missing. ci-noir passes allow_push: true since it only
triggers on schedule and dispatch.
---
 .github/workflows/build-ci-image.yaml | 63 ++++++++++++++++++++-------
 .github/workflows/ci-noir.yaml        |  2 +-
 scripts/ci/verify_ci_image.py         | 29 ------------
 3 files changed, 49 insertions(+), 45 deletions(-)
 delete mode 100644 scripts/ci/verify_ci_image.py

diff --git a/.github/workflows/build-ci-image.yaml b/.github/workflows/build-ci-image.yaml
index c7d17baf..00733ccc 100644
--- a/.github/workflows/build-ci-image.yaml
+++ b/.github/workflows/build-ci-image.yaml
@@ -7,18 +7,22 @@ on:
         type: boolean
     outputs:
       image_tag:
-        value: ${{ jobs.build.outputs.image_tag }}
+        value: ${{ jobs.check.outputs.image_tag }}
 
 permissions:
   contents: read
   packages: write
 
 jobs:
-  build:
-    name: Build CI Image
+  check:
+    name: Check CI Image
     runs-on: ubuntu-latest
     outputs:
       image_tag: ${{ steps.versions.outputs.image_tag }}
+      exists: ${{ steps.exists.outputs.exists }}
+      rust_stable: ${{ steps.versions.outputs.rust_stable }}
+      lean_toolchain: ${{ steps.versions.outputs.lean_toolchain }}
+      noir_rev: ${{ steps.versions.outputs.noir_rev }}
     steps:
       - name: Checkout
         uses: actions/checkout@v6
@@ -31,15 +35,38 @@ jobs:
           registry: ghcr.io
           username: ${{ github.actor }}
           password: ${{ secrets.GITHUB_TOKEN }}
-      - name: Check CI Image
-        id: check
+      - name: Probe Image Manifest
+        id: probe
         continue-on-error: true
-        run: python3 scripts/ci/verify_ci_image.py ghcr.io/reilabs/lampe-ci:${{ steps.versions.outputs.image_tag }}
+        run: docker manifest inspect ghcr.io/reilabs/lampe-ci:${{ steps.versions.outputs.image_tag }} > /dev/null
+      - name: Record Image Existence
+        id: exists
+        run: |
+          if [ "${{ steps.probe.outcome }}" = "success" ]; then
+            echo "exists=true" >> "$GITHUB_OUTPUT"
+          else
+            echo "exists=false" >> "$GITHUB_OUTPUT"
+          fi
+
+  build:
+    name: Build And Push CI Image
+    needs: check
+    if: needs.check.outputs.exists != 'true' && inputs.allow_push
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v6
+      - name: Free Runner Disk Space
+        uses: ./.github/actions/free-disk-space
+      - name: Log In To GHCR
+        uses: docker/login-action@v3
+        with:
+          registry: ghcr.io
+          username: ${{ github.actor }}
+          password: ${{ secrets.GITHUB_TOKEN }}
       - name: Set Up Docker Buildx
-        if: steps.check.outcome == 'failure' && inputs.allow_push
         uses: docker/setup-buildx-action@v3
       - name: Build And Push Image
-        if: steps.check.outcome == 'failure' && inputs.allow_push
         uses: docker/build-push-action@v6
         with:
           context: .
@@ -49,13 +76,19 @@ jobs:
           tags: |
             ghcr.io/reilabs/lampe-ci:latest
             ghcr.io/reilabs/lampe-ci:sha-${{ github.sha }}
-            ghcr.io/reilabs/lampe-ci:${{ steps.versions.outputs.image_tag }}
+            ghcr.io/reilabs/lampe-ci:${{ needs.check.outputs.image_tag }}
           build-args: |
-            RUST_TOOLCHAIN_STABLE=${{ steps.versions.outputs.rust_stable }}
-            LEAN_TOOLCHAIN=${{ steps.versions.outputs.lean_toolchain }}
-            NOIR_REV=${{ steps.versions.outputs.noir_rev }}
-      - name: Fail If Image Missing
-        if: steps.check.outcome == 'failure' && !inputs.allow_push
+            RUST_TOOLCHAIN_STABLE=${{ needs.check.outputs.rust_stable }}
+            LEAN_TOOLCHAIN=${{ needs.check.outputs.lean_toolchain }}
+            NOIR_REV=${{ needs.check.outputs.noir_rev }}
+
+  guard:
+    name: Fail If Image Missing
+    needs: check
+    if: needs.check.outputs.exists != 'true' && !inputs.allow_push
+    runs-on: ubuntu-latest
+    steps:
+      - name: Report Missing Image
         run: |
-          echo "CI image ghcr.io/reilabs/lampe-ci:${{ steps.versions.outputs.image_tag }} is missing and cannot be built from a fork."
+          echo "CI image ghcr.io/reilabs/lampe-ci:${{ needs.check.outputs.image_tag }} is missing and cannot be built from a fork."
           exit 1
diff --git a/.github/workflows/ci-noir.yaml b/.github/workflows/ci-noir.yaml
index 51693d23..c53027ad 100644
--- a/.github/workflows/ci-noir.yaml
+++ b/.github/workflows/ci-noir.yaml
@@ -12,7 +12,7 @@ jobs:
   build-ci-image:
     uses: ./.github/workflows/build-ci-image.yaml
     with:
-      allow_push: ${{ github.event_name != 'pull_request' || github.event.pull_request.head.repo.full_name == github.repository }}
+      allow_push: true
   
   run-tests:
     name: Test Noir
diff --git a/scripts/ci/verify_ci_image.py b/scripts/ci/verify_ci_image.py
deleted file mode 100644
index 0268605c..00000000
--- a/scripts/ci/verify_ci_image.py
+++ /dev/null
@@ -1,29 +0,0 @@
-#!/usr/bin/env python3
-import argparse
-import subprocess
-import sys
-
-
-def main() -> None:
-    parser = argparse.ArgumentParser(description="Verify CI image exists in GHCR")
-    parser.add_argument("image", help="Full image reference (ghcr.io/org/name:tag)")
-    args = parser.parse_args()
-
-    try:
-        subprocess.run(
-            ["docker", "manifest", "inspect", args.image],
-            check=True,
-            stdout=subprocess.DEVNULL,
-            stderr=subprocess.DEVNULL,
-        )
-    except subprocess.CalledProcessError:
-        message = (
-            "CI image not found: {image}\n"
-            "Run the CI Image workflow to publish it before re-running CI.\n"
-        ).format(image=args.image)
-        sys.stderr.write(message)
-        raise SystemExit(1)
-
-
-if __name__ == "__main__":
-    main()

From aa379d7a35ab087577961df3c6d764e4af6d7411 Mon Sep 17 00:00:00 2001
From: Eduardo Gomes <eduardogbg@gmail.com>
Date: Thu, 11 Jun 2026 16:16:49 -0300
Subject: [PATCH 4/8] scripts: share lake package clones and keep dep rewrites
 byte-preserving

scripts/ci/link_lake_packages.py points a workspace's .lake/packages at
the shared $LAKE_PKG_DIR; test.xsh and the CI jobs invoke the same
helper. The lakefile/manifest rewriters only write when something
actually changes, since CI cache keys hash the rewritten files.
'lake exe cache get' is best-effort: the baked store restores offline
and 'lake build' can always finish from source. Tests run in sorted
order, and the single-purpose helpers in utils.xsh fold into the
regex-based ones.
---
 .gitignore                       |  1 +
 scripts/ci/link_lake_packages.py | 43 ++++++++++++++++++++++++
 scripts/test.xsh                 | 45 ++++++++++++-------------
 scripts/utils.xsh                | 56 ++++++++------------------------
 testing_noir/test.xsh            |  3 +-
 5 files changed, 79 insertions(+), 69 deletions(-)
 create mode 100755 scripts/ci/link_lake_packages.py

diff --git a/.gitignore b/.gitignore
index d8c9b8cf..f817b650 100644
--- a/.gitignore
+++ b/.gitignore
@@ -5,5 +5,6 @@
 /target
 .idea
 .vscode
+__pycache__/
 
 testing/MerkleFromScratch/lampe/lake-manifest.json
diff --git a/scripts/ci/link_lake_packages.py b/scripts/ci/link_lake_packages.py
new file mode 100755
index 00000000..2810d5c3
--- /dev/null
+++ b/scripts/ci/link_lake_packages.py
@@ -0,0 +1,43 @@
+#!/usr/bin/env python3
+"""Symlink <lampe_dir>/.lake/packages at the shared $LAKE_PKG_DIR.
+
+Pointing each workspace's `.lake/packages` at the shared dir lets every
+lake invocation in a CI run reuse the same mathlib / proven-zk / batteries
+clones. The lakefile and manifest both spell the dir as `.lake/packages`,
+so the symlink is enough; no further rewriting is required. A no-op when
+LAKE_PKG_DIR is unset.
+"""
+import os
+import pathlib
+import shutil
+import sys
+
+
+def link_packages_dir(lampe_dir: pathlib.Path) -> None:
+    packages_root_env = os.environ.get("LAKE_PKG_DIR")
+    if not packages_root_env:
+        return
+    packages_root = pathlib.Path(packages_root_env)
+    packages_root.mkdir(parents=True, exist_ok=True)
+    lake_dir = lampe_dir / ".lake"
+    lake_dir.mkdir(parents=True, exist_ok=True)
+    packages_link = lake_dir / "packages"
+    if packages_link.is_symlink() or packages_link.exists():
+        if packages_link.is_symlink() or not packages_link.is_dir():
+            packages_link.unlink()
+        else:
+            shutil.rmtree(packages_link)
+    packages_link.symlink_to(
+        os.path.relpath(packages_root, lake_dir),
+        target_is_directory=True,
+    )
+
+
+def main() -> None:
+    if len(sys.argv) != 2:
+        raise SystemExit(f"usage: {sys.argv[0]} <lampe_dir>")
+    link_packages_dir(pathlib.Path(sys.argv[1]))
+
+
+if __name__ == "__main__":
+    main()
diff --git a/scripts/test.xsh b/scripts/test.xsh
index a4e77c0b..8e3d1023 100755
--- a/scripts/test.xsh
+++ b/scripts/test.xsh
@@ -4,7 +4,6 @@ import argparse
 from pathlib import Path
 import os
 import re
-import shutil
 import subprocess
 import sys
 
@@ -93,7 +92,7 @@ def run_tests(dir):
 
     if selected_test == "":
         test_cases = []
-        for item in test_cases_dir.iterdir():
+        for item in sorted(test_cases_dir.iterdir()):
             if item.is_dir() and not item.name.startswith('.') and item != test_cases_dir:
                 test_cases.append(item)
     else:
@@ -184,8 +183,8 @@ def _git(args, capture=False):
     )
 
 def assert_extraction_matches(test_dir):
-    # We now run extraction in-place under the checked-in test directory,
-    # so reproducibility is checked by asking git whether the working tree
+    # Extraction runs in-place under the checked-in test directory, so
+    # reproducibility is checked by asking git whether the working tree
     # under that directory matches HEAD.
     #
     # Files we deliberately do NOT compare:
@@ -193,7 +192,7 @@ def assert_extraction_matches(test_dir):
     #   - lakefile.toml   -> the CLI is allowed to regenerate it but the
     #                        path = "..." entries for Lampe/stdlib may be
     #                        formatted slightly differently than what is
-    #                        checked in; the old diff also excluded this.
+    #                        checked in.
     #   - lake-manifest.json -> lake resolves it at build time from inputRev.
     rel = test_dir.relative_to(project_root)
     pathspecs = [
@@ -223,7 +222,13 @@ def assert_extraction_matches(test_dir):
         )
 
 def build_lake(lampe_dir):
-    subprocess.run(["lake", "exe", "cache", "get"], check=True, cwd=lampe_dir)
+    # `cache get` is best-effort recovery, not a hard dependency. In CI the
+    # image bakes a complete `.ltar` store at $MATHLIB_CACHE_DIR, so this is
+    # an offline restore of mathlib oleans into whatever clones lake
+    # materialized under the shared $LAKE_PKG_DIR; locally the cloud cache
+    # may not serve the pinned revision at all. Either way `lake build` can
+    # always finish from source, so a failure here must not fail the test.
+    subprocess.run(["lake", "exe", "cache", "get"], check=False, cwd=lampe_dir)
     subprocess.run(["lake", "build"], check=True, cwd=lampe_dir)
 
 def rewrite_lampe_stdlib_deps_to_path(lampe_dir):
@@ -254,25 +259,15 @@ def rewrite_lampe_stdlib_deps_to_path(lampe_dir):
 def link_packages_dir(lampe_dir):
     # Point each test's `.lake/packages` at the shared `$LAKE_PKG_DIR`
     # cache so consecutive tests reuse the same mathlib / proven-zk /
-    # batteries clones. The lakefile and manifest both spell the dir as
-    # `.lake/packages`, so the symlink is enough; no further rewriting
-    # is required for the package cache to work.
-    packages_root_env = os.environ.get("LAKE_PKG_DIR")
-    if not packages_root_env:
-        return
-    packages_root = Path(packages_root_env)
-    packages_root.mkdir(parents=True, exist_ok=True)
-    lake_dir = lampe_dir / ".lake"
-    lake_dir.mkdir(parents=True, exist_ok=True)
-    packages_link = lake_dir / "packages"
-    if packages_link.is_symlink() or packages_link.exists():
-        if packages_link.is_symlink() or not packages_link.is_dir():
-            packages_link.unlink()
-        else:
-            shutil.rmtree(packages_link)
-    packages_link.symlink_to(
-        os.path.relpath(packages_root, lake_dir),
-        target_is_directory=True,
+    # batteries clones. The symlink logic lives in the helper script so
+    # CI workflow steps can run the same thing.
+    subprocess.run(
+        [
+            sys.executable,
+            str(project_root / "scripts" / "ci" / "link_lake_packages.py"),
+            str(lampe_dir),
+        ],
+        check=True,
     )
 
 def run_test(dir_path, update_mode):
diff --git a/scripts/utils.xsh b/scripts/utils.xsh
index da992f8a..d59519f7 100644
--- a/scripts/utils.xsh
+++ b/scripts/utils.xsh
@@ -35,7 +35,6 @@ except NameError:
     project_root = get_project_root()
 # --- End of copied part.
 
-lakefile_toml_path = project_root / 'testing' / 'MerkleFromScratch' / 'lampe' / 'lakefile.toml'
 rust_cargo_toml_path = project_root / 'Cargo.toml'
 ci_noir_yaml_path = project_root / '.github' / 'workflows' / 'ci-noir.yaml'
 
@@ -55,22 +54,6 @@ def write_json(path, data):
     with open(path, mode="w") as f:
         json.dump(data, f, indent=1)
 
-def set_packages_dir(toml, packages_dir):
-    toml['packagesDir'] = packages_dir
-    return toml
-
-def set_toml_packages_dir(toml_path, packages_dir):
-    lakefile_toml = load_toml(toml_path)
-
-    set_packages_dir(lakefile_toml, packages_dir)
-
-    write_toml(toml_path, lakefile_toml)
-
-def set_manifest_packages_dir(manifest_path, packages_dir):
-    manifest = load_json(manifest_path)
-    manifest['packagesDir'] = packages_dir
-    write_json(manifest_path, manifest)
-
 def load_yaml(path):
     with open(path, mode="r") as f:
         return yaml.safe_load(f)
@@ -92,47 +75,36 @@ def change_required_dep_to_path_by_regex(toml, name_regex, path):
 
     return toml
 
+# The rewrite helpers below only write when they actually change something:
+# several CI cache keys hash the rewritten files (lakefile.toml,
+# lake-manifest.json), and a byte-changing no-op write (e.g. re-serializing
+# a manifest that lake formatted differently) silently changes those keys
+# between restore and save.
 def change_toml_required_dep_to_path_by_regex(toml_path, name_regex, path):
     lakefile_toml = load_toml(toml_path)
+    original = dumps(lakefile_toml)
 
     change_required_dep_to_path_by_regex(lakefile_toml, name_regex, path)
 
-    write_toml(toml_path, lakefile_toml)
-
-def change_required_lampe_to_path(toml, path):
-    for i, v in enumerate(toml['require']):
-        if v['name'] != 'Lampe':
-                continue
-
-        keys = list(v.keys())
-        for key in keys:
-            if key == 'name':
-                    continue
-            del v[key]
-
-        v['path'] = path
-
-    return toml
-
-def change_toml_required_lampe_to_path(toml_path, lampe_path):
-    lakefile_toml = load_toml(toml_path)
-
-    change_required_lampe_to_path(lakefile_toml, lampe_path)
-
-    write_toml(toml_path, lakefile_toml)
+    if dumps(lakefile_toml) != original:
+        write_toml(toml_path, lakefile_toml)
 
 def change_manifest_required_dep_to_path_by_regex(manifest_path, name_regex, path):
     manifest = load_json(manifest_path)
     compiled_name_regex = re.compile(name_regex)
+    changed = False
 
     for package in manifest.get('packages', []):
         if not compiled_name_regex.match(package.get('name', '')):
             continue
         if package.get('type') != 'path':
             continue
-        package['dir'] = path
+        if package.get('dir') != path:
+            package['dir'] = path
+            changed = True
 
-    write_json(manifest_path, manifest)
+    if changed:
+        write_json(manifest_path, manifest)
 
 def read_noir_version():
     rust_cargo_toml = load_toml(rust_cargo_toml_path)
diff --git a/testing_noir/test.xsh b/testing_noir/test.xsh
index ccf24532..5f590cd2 100755
--- a/testing_noir/test.xsh
+++ b/testing_noir/test.xsh
@@ -57,7 +57,6 @@ def parse_args():
 def prepare_lampe(lake_cmd):
     """Build a local version of lampe if use_local is set"""
     pushd @(project_root / "Lampe")
-    $(@(lake_cmd) exe cache get)
     $(@(lake_cmd) build)
     popd
 
@@ -110,7 +109,7 @@ def process_test(test_dir, lake_dir, log_file, lampe_cmd, lake_cmd, log_stdout,
             lakefile_path = Path("lakefile.toml")
             lakefile_lampe_relative_path = "../../../Lampe"
 
-            change_toml_required_lampe_to_path(lakefile_path, lakefile_lampe_relative_path)
+            change_toml_required_dep_to_path_by_regex(lakefile_path, '^Lampe$', lakefile_lampe_relative_path)
 
             $(@(lake_cmd) update)
 

From 69c290e09e033ce454679bb4febb1ff369de6913 Mon Sep 17 00:00:00 2001
From: Eduardo Gomes <eduardogbg@gmail.com>
Date: Thu, 11 Jun 2026 16:17:00 -0300
Subject: [PATCH 5/8] testing: pin every project's manifest with one mathlib
 URL spelling

Checked-in lake-manifest.json files keep lake from re-resolving mathlib
through proven-zk's .git-suffixed URL spelling and discarding existing
clones. MerkleFromScratch drops its packagesDir override in favor of
the shared packages symlink.
---
 .gitignore                                    |   2 -
 .../Merkle/hasher/lampe/lake-manifest.json    | 109 ++++++++++++++++
 .../Merkle/merkle/lampe/lake-manifest.json    |   2 +-
 .../skyscraper/lampe/lake-manifest.json       |   2 +-
 .../lampe/lake-manifest.json                  | 119 ++++++++++++++++++
 testing/MerkleFromScratch/lampe/lakefile.toml |   1 -
 6 files changed, 230 insertions(+), 5 deletions(-)
 create mode 100644 testing/Merkle/hasher/lampe/lake-manifest.json
 create mode 100644 testing/MerkleFromScratch/lampe/lake-manifest.json

diff --git a/.gitignore b/.gitignore
index f817b650..d119c0e8 100644
--- a/.gitignore
+++ b/.gitignore
@@ -6,5 +6,3 @@
 .idea
 .vscode
 __pycache__/
-
-testing/MerkleFromScratch/lampe/lake-manifest.json
diff --git a/testing/Merkle/hasher/lampe/lake-manifest.json b/testing/Merkle/hasher/lampe/lake-manifest.json
new file mode 100644
index 00000000..f94a88b2
--- /dev/null
+++ b/testing/Merkle/hasher/lampe/lake-manifest.json
@@ -0,0 +1,109 @@
+{"version": "1.1.0",
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"type": "path",
+   "scope": "",
+   "name": "«std-1.0.0-beta.14»",
+   "manifestFile": "lake-manifest.json",
+   "inherited": false,
+   "dir": "../../../../stdlib/lampe",
+   "configFile": "lakefile.toml"},
+  {"type": "path",
+   "scope": "",
+   "name": "Lampe",
+   "manifestFile": "lake-manifest.json",
+   "inherited": false,
+   "dir": "../../../../Lampe",
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/batteries",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "756e3321fd3b02a85ffda19fef789916223e578c",
+   "name": "batteries",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.29.1",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/mathlib4",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "5e932f97dd25535344f80f9dd8da3aab83df0fe6",
+   "name": "mathlib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.29.1",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/plausible",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "83e90935a17ca19ebe4b7893c7f7066e266f50d3",
+   "name": "plausible",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/LeanSearchClient",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843",
+   "name": "LeanSearchClient",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/import-graph",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "48d5698bc464786347c1b0d859b18f938420f060",
+   "name": "importGraph",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/ProofWidgets4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "4dd0959c44d1af0462bd604d0f87c5781307d709",
+   "name": "proofwidgets",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v0.0.95+lean-v4.29.1",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/aesop",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "7152850e7b216a0d409701617721b6e469d34bf6",
+   "name": "aesop",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/quote4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "707efb56d0696634e9e965523a1bbe9ac6ce141d",
+   "name": "Qq",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover",
+   "rev": "7802da01beb530bf051ab657443f9cd9bc3e1a29",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.29.0",
+   "inherited": true,
+   "configFile": "lakefile.toml"}],
+ "name": "«hasher-0.0.0»",
+ "lakeDir": ".lake"}
diff --git a/testing/Merkle/merkle/lampe/lake-manifest.json b/testing/Merkle/merkle/lampe/lake-manifest.json
index 4aa8b144..23ddcf7b 100644
--- a/testing/Merkle/merkle/lampe/lake-manifest.json
+++ b/testing/Merkle/merkle/lampe/lake-manifest.json
@@ -39,7 +39,7 @@
    "inherited": false,
    "dir": "../../../../Lampe",
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/mathlib4.git",
+  {"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
    "scope": "",
diff --git a/testing/Merkle/skyscraper/lampe/lake-manifest.json b/testing/Merkle/skyscraper/lampe/lake-manifest.json
index 2132b6aa..46a24176 100644
--- a/testing/Merkle/skyscraper/lampe/lake-manifest.json
+++ b/testing/Merkle/skyscraper/lampe/lake-manifest.json
@@ -32,7 +32,7 @@
    "inherited": false,
    "dir": "../../../../Lampe",
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/mathlib4.git",
+  {"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
    "scope": "",
diff --git a/testing/MerkleFromScratch/lampe/lake-manifest.json b/testing/MerkleFromScratch/lampe/lake-manifest.json
new file mode 100644
index 00000000..95d0abac
--- /dev/null
+++ b/testing/MerkleFromScratch/lampe/lake-manifest.json
@@ -0,0 +1,119 @@
+{"version": "1.1.0",
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"url": "https://github.com/reilabs/proven-zk",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "fd156e1a0a0771271b7871972f428b0c93b5b56e",
+   "name": "«proven-zk»",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "fd156e1a0a0771271b7871972f428b0c93b5b56e",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"type": "path",
+   "scope": "",
+   "name": "«std-1.0.0-beta.14»",
+   "manifestFile": "lake-manifest.json",
+   "inherited": false,
+   "dir": "../../../stdlib/lampe",
+   "configFile": "lakefile.toml"},
+  {"type": "path",
+   "scope": "",
+   "name": "Lampe",
+   "manifestFile": "lake-manifest.json",
+   "inherited": false,
+   "dir": "../../../Lampe",
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/mathlib4",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "5e932f97dd25535344f80f9dd8da3aab83df0fe6",
+   "name": "mathlib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.29.1",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/plausible",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "83e90935a17ca19ebe4b7893c7f7066e266f50d3",
+   "name": "plausible",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/LeanSearchClient",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843",
+   "name": "LeanSearchClient",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/import-graph",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "48d5698bc464786347c1b0d859b18f938420f060",
+   "name": "importGraph",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/ProofWidgets4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "4dd0959c44d1af0462bd604d0f87c5781307d709",
+   "name": "proofwidgets",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v0.0.95+lean-v4.29.1",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/aesop",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "7152850e7b216a0d409701617721b6e469d34bf6",
+   "name": "aesop",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/quote4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "707efb56d0696634e9e965523a1bbe9ac6ce141d",
+   "name": "Qq",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/batteries",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "756e3321fd3b02a85ffda19fef789916223e578c",
+   "name": "batteries",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover",
+   "rev": "7802da01beb530bf051ab657443f9cd9bc3e1a29",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.29.0",
+   "inherited": true,
+   "configFile": "lakefile.toml"}],
+ "name": "«Merkle-1.0.0»",
+ "lakeDir": ".lake"}
diff --git a/testing/MerkleFromScratch/lampe/lakefile.toml b/testing/MerkleFromScratch/lampe/lakefile.toml
index d97b1730..0faa1d32 100644
--- a/testing/MerkleFromScratch/lampe/lakefile.toml
+++ b/testing/MerkleFromScratch/lampe/lakefile.toml
@@ -1,7 +1,6 @@
 # Generated by lampe
 name = "Merkle-1.0.0"
 version = "1.0.0"
-packagesDir = "../../../.lake/packages"
 defaultTargets = ["Merkle-1.0.0"]
 
 [[lean_lib]]

From 739f83d166573ce6c5c368079a458324d1cc6f21 Mon Sep 17 00:00:00 2001
From: Eduardo Gomes <eduardogbg@gmail.com>
Date: Thu, 11 Jun 2026 16:17:16 -0300
Subject: [PATCH 6/8] ci: compute cache keys once and gate jobs at the job
 level

A keys job computes every cache key in one place and probes them with
lookup-only restores; the rustfmt/clippy/test/lean/stdlib/e2e jobs skip
at the job level on an exact hit, with !failure() && !cancelled()
guards on jobs downstream of skippable ones. Lean jobs share dependency
clones via $LAKE_PKG_DIR and restore builds through restore-keys
fallbacks, so lake builds stay incremental on partial hits. The CLI
travels between jobs only as an artifact (upload zips drop the exec
bit, hence the chmod steps). The unused CI_IMAGE env var is gone.
---
 .github/workflows/ci.yaml | 318 +++++++++++++++-----------------------
 1 file changed, 124 insertions(+), 194 deletions(-)

diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml
index 6c556098..70d5be4e 100644
--- a/.github/workflows/ci.yaml
+++ b/.github/workflows/ci.yaml
@@ -16,12 +16,85 @@ jobs:
     with:
       allow_push: ${{ github.event_name != 'pull_request' || github.event.pull_request.head.repo.full_name == github.repository }}
 
+  keys:
+    name: Compute Cache Keys
+    runs-on: ubuntu-latest
+    outputs:
+      rustfmt_key: ${{ steps.keys.outputs.rustfmt_key }}
+      rustlint_key: ${{ steps.keys.outputs.rustlint_key }}
+      rusttest_key: ${{ steps.keys.outputs.rusttest_key }}
+      cli_key: ${{ steps.keys.outputs.cli_key }}
+      lampe_key: ${{ steps.keys.outputs.lampe_key }}
+      stdlib_key: ${{ steps.keys.outputs.stdlib_key }}
+      e2e_key: ${{ steps.keys.outputs.e2e_key }}
+      rustfmt_hit: ${{ steps.rustfmt.outputs.cache-hit }}
+      rustlint_hit: ${{ steps.rustlint.outputs.cache-hit }}
+      rusttest_hit: ${{ steps.rusttest.outputs.cache-hit }}
+      e2e_hit: ${{ steps.e2e.outputs.cache-hit }}
+      lampe_hit: ${{ steps.lampe.outputs.cache-hit }}
+      stdlib_hit: ${{ steps.stdlib.outputs.cache-hit }}
+    steps:
+      - name: Checkout Current Branch
+        uses: actions/checkout@v6
+      - name: Compute Keys
+        id: keys
+        run: |
+          {
+            echo "rustfmt_key=rustfmt-${{ runner.os }}-${{ hashFiles('Cargo.toml', 'Cargo.lock', 'rust-toolchain.toml', 'src/**') }}"
+            echo "rustlint_key=rustlint-${{ runner.os }}-${{ hashFiles('Cargo.toml', 'Cargo.lock', 'rust-toolchain.toml', 'src/**') }}"
+            echo "rusttest_key=rusttest-${{ runner.os }}-${{ hashFiles('Cargo.toml', 'Cargo.lock', 'rust-toolchain.toml', 'src/**') }}"
+            echo "cli_key=cli-${{ runner.os }}-${{ hashFiles('Cargo.toml', 'Cargo.lock', 'rust-toolchain.toml', 'src/**', 'Lampe/lean-toolchain') }}"
+            echo "lampe_key=lampe-build-${{ runner.os }}-${{ hashFiles('Lampe/**/*.lean', 'Lampe/**/*.toml', 'Lampe/**/*.json', 'Lampe/lean-toolchain', 'Lampe/lake-manifest.json') }}"
+            echo "stdlib_key=stdlib-build-${{ runner.os }}-${{ hashFiles('stdlib/src/**', 'stdlib/Nargo.toml', 'stdlib/test.xsh', 'stdlib/lampe/**/*.lean', 'stdlib/lampe/lean-toolchain', 'stdlib/lampe/lake-manifest.json', 'stdlib/lampe/lakefile.toml', 'Lampe/**/*.lean', 'Lampe/**/*.toml', 'Lampe/**/*.json', 'Lampe/lean-toolchain', 'Lampe/lake-manifest.json', 'scripts/test.xsh', 'scripts/utils.xsh', 'Cargo.toml', 'Cargo.lock', 'rust-toolchain.toml', 'src/**') }}"
+            echo "e2e_key=e2e-${{ runner.os }}-${{ hashFiles('testing/**', 'scripts/test.xsh', 'scripts/utils.xsh', 'Cargo.toml', 'Cargo.lock', 'rust-toolchain.toml', 'src/**', 'Lampe/**/*.lean', 'Lampe/**/*.toml', 'Lampe/**/*.json', 'Lampe/lean-toolchain', 'Lampe/lake-manifest.json', 'stdlib/src/**', 'stdlib/Nargo.toml', 'stdlib/lampe/**/*.lean', 'stdlib/lampe/lean-toolchain', 'stdlib/lampe/lake-manifest.json', 'stdlib/lampe/lakefile.toml', '!**/.lake/**') }}"
+          } >> "$GITHUB_OUTPUT"
+      - name: Probe Rustfmt Cache
+        id: rustfmt
+        uses: actions/cache/restore@v5
+        with:
+          path: .ci-cache/rustfmt
+          key: ${{ steps.keys.outputs.rustfmt_key }}
+          lookup-only: true
+      - name: Probe Rust Lint Cache
+        id: rustlint
+        uses: actions/cache/restore@v5
+        with:
+          path: .ci-cache/rustlint
+          key: ${{ steps.keys.outputs.rustlint_key }}
+          lookup-only: true
+      - name: Probe Rust Test Cache
+        id: rusttest
+        uses: actions/cache/restore@v5
+        with:
+          path: .ci-cache/rusttest
+          key: ${{ steps.keys.outputs.rusttest_key }}
+          lookup-only: true
+      - name: Probe E2E Cache
+        id: e2e
+        uses: actions/cache/restore@v5
+        with:
+          path: .ci-cache/e2e
+          key: ${{ steps.keys.outputs.e2e_key }}
+          lookup-only: true
+      - name: Probe Lampe Build Cache
+        id: lampe
+        uses: actions/cache/restore@v5
+        with:
+          path: Lampe/.lake/build
+          key: ${{ steps.keys.outputs.lampe_key }}
+          lookup-only: true
+      - name: Probe Stdlib Build Cache
+        id: stdlib
+        uses: actions/cache/restore@v5
+        with:
+          path: stdlib/lampe/.lake/build
+          key: ${{ steps.keys.outputs.stdlib_key }}
+          lookup-only: true
+
   ensure-noir-version:
     name: Check Noir Versions
     needs: build-ci-image
     runs-on: ubuntu-latest
-    env:
-      CI_IMAGE: ghcr.io/reilabs/lampe-ci:${{ needs.build-ci-image.outputs.image_tag }}
     container:
       image: ghcr.io/reilabs/lampe-ci:${{ needs.build-ci-image.outputs.image_tag }}
       credentials:
@@ -35,10 +108,9 @@ jobs:
 
   check-rust-formatting:
     name: Check Rust Formatting
-    needs: [build-ci-image]
+    needs: [build-ci-image, keys]
+    if: needs.keys.outputs.rustfmt_hit != 'true'
     runs-on: ubuntu-latest
-    env:
-      CI_IMAGE: ghcr.io/reilabs/lampe-ci:${{ needs.build-ci-image.outputs.image_tag }}
     container:
       image: ghcr.io/reilabs/lampe-ci:${{ needs.build-ci-image.outputs.image_tag }}
       credentials:
@@ -49,27 +121,23 @@ jobs:
         uses: actions/checkout@v6
         with:
           submodules: recursive
-      - name: Restore Rustfmt Cache
-        id: rustfmt-cache
-        uses: actions/cache@v5
-        with:
-          path: .ci-cache/rustfmt
-          key: rustfmt-${{ runner.os }}-${{ hashFiles('Cargo.toml', 'Cargo.lock', 'rust-toolchain.toml', 'src/**') }}
       - name: Check Formatting
-        if: ${{ steps.rustfmt-cache.outputs.cache-hit != 'true' }}
         run: cargo +nightly fmt --all -- --check
       - name: Mark Rustfmt Cache
-        if: ${{ steps.rustfmt-cache.outputs.cache-hit != 'true' }}
         run: |
           mkdir -p .ci-cache/rustfmt
           echo "ok" > .ci-cache/rustfmt/success
+      - name: Save Rustfmt Cache
+        uses: actions/cache/save@v5
+        with:
+          path: .ci-cache/rustfmt
+          key: ${{ needs.keys.outputs.rustfmt_key }}
 
   lint-rust:
     name: Lint Rust
-    needs: [build-ci-image]
+    needs: [build-ci-image, keys]
+    if: needs.keys.outputs.rustlint_hit != 'true'
     runs-on: ubuntu-latest
-    env:
-      CI_IMAGE: ghcr.io/reilabs/lampe-ci:${{ needs.build-ci-image.outputs.image_tag }}
     container:
       image: ghcr.io/reilabs/lampe-ci:${{ needs.build-ci-image.outputs.image_tag }}
       credentials:
@@ -78,27 +146,23 @@ jobs:
     steps:
       - name: Checkout Current Branch
         uses: actions/checkout@v6
-      - name: Restore Rust Lint Cache
-        id: rustlint-cache
-        uses: actions/cache@v5
-        with:
-          path: .ci-cache/rustlint
-          key: rustlint-${{ runner.os }}-${{ hashFiles('Cargo.toml', 'Cargo.lock', 'rust-toolchain.toml', 'src/**') }}
       - name: Lint (Clippy)
-        if: ${{ steps.rustlint-cache.outputs.cache-hit != 'true' }}
         run: RUSTFLAGS="-Dwarnings" cargo clippy --all-targets --all-features
       - name: Mark Rust Lint Cache
-        if: ${{ steps.rustlint-cache.outputs.cache-hit != 'true' }}
         run: |
           mkdir -p .ci-cache/rustlint
           echo "ok" > .ci-cache/rustlint/success
+      - name: Save Rust Lint Cache
+        uses: actions/cache/save@v5
+        with:
+          path: .ci-cache/rustlint
+          key: ${{ needs.keys.outputs.rustlint_key }}
 
   test-rust:
     name: Test Rust
-    needs: [build-ci-image]
+    needs: [build-ci-image, keys]
+    if: needs.keys.outputs.rusttest_hit != 'true'
     runs-on: ubuntu-latest
-    env:
-      CI_IMAGE: ghcr.io/reilabs/lampe-ci:${{ needs.build-ci-image.outputs.image_tag }}
     container:
       image: ghcr.io/reilabs/lampe-ci:${{ needs.build-ci-image.outputs.image_tag }}
       credentials:
@@ -107,30 +171,25 @@ jobs:
     steps:
       - name: Checkout Current Branch
         uses: actions/checkout@v6
-      - name: Restore Rust Test Cache
-        id: rusttest-cache
-        uses: actions/cache@v5
-        with:
-          path: .ci-cache/rusttest
-          key: rusttest-${{ runner.os }}-${{ hashFiles('Cargo.toml', 'Cargo.lock', 'rust-toolchain.toml', 'src/**') }}
       - name: Test (Cargo)
-        if: ${{ steps.rusttest-cache.outputs.cache-hit != 'true' }}
         run: cargo test --all
       - name: Remove Build Artifacts
-        if: ${{ steps.rusttest-cache.outputs.cache-hit != 'true' }}
         run: rm -rf target
       - name: Mark Rust Test Cache
-        if: ${{ steps.rusttest-cache.outputs.cache-hit != 'true' }}
         run: |
           mkdir -p .ci-cache/rusttest
           echo "ok" > .ci-cache/rusttest/success
+      - name: Save Rust Test Cache
+        uses: actions/cache/save@v5
+        with:
+          path: .ci-cache/rusttest
+          key: ${{ needs.keys.outputs.rusttest_key }}
 
   build-rust:
     name: Build CLI
-    needs: [build-ci-image, check-rust-formatting, lint-rust, test-rust]
+    needs: [build-ci-image, keys, check-rust-formatting, lint-rust, test-rust]
+    if: ${{ !failure() && !cancelled() }}
     runs-on: ubuntu-latest
-    env:
-      CI_IMAGE: ghcr.io/reilabs/lampe-ci:${{ needs.build-ci-image.outputs.image_tag }}
     container:
       image: ghcr.io/reilabs/lampe-ci:${{ needs.build-ci-image.outputs.image_tag }}
       credentials:
@@ -144,12 +203,11 @@ jobs:
         uses: actions/cache@v5
         with:
           path: target/release/lampe
-          key: cli-${{ runner.os }}-${{ hashFiles('Cargo.toml', 'Cargo.lock', 'rust-toolchain.toml', 'src/**', 'Lampe/lean-toolchain') }}
+          key: ${{ needs.keys.outputs.cli_key }}
       - name: Build (Cargo)
         if: ${{ steps.cli-cache.outputs.cache-hit != 'true' }}
         run: cargo build --release
       - name: Upload CLI Artifact
-        if: ${{ steps.cli-cache.outputs.cache-hit != 'true' }}
         uses: actions/upload-artifact@v4
         with:
           name: lampe-cli-${{ github.sha }}
@@ -157,10 +215,9 @@ jobs:
 
   build-lean:
     name: Build Lampe
-    needs: [build-ci-image]
+    needs: [build-ci-image, keys]
+    if: needs.keys.outputs.lampe_hit != 'true'
     runs-on: ubuntu-latest
-    env:
-      CI_IMAGE: ghcr.io/reilabs/lampe-ci:${{ needs.build-ci-image.outputs.image_tag }}
     container:
       image: ghcr.io/reilabs/lampe-ci:${{ needs.build-ci-image.outputs.image_tag }}
       credentials:
@@ -172,64 +229,40 @@ jobs:
         with:
           sparse-checkout: |
             Lampe
+            scripts/ci
             stdlib/lampe/lean-toolchain
             stdlib/lampe/lake-manifest.json
       - name: Set Lake Package Dir
         run: |
           mkdir -p "$RUNNER_TEMP/lake-packages"
           echo "LAKE_PKG_DIR=$RUNNER_TEMP/lake-packages" >> "$GITHUB_ENV"
-      - name: Restore Lake Packages Cache
-        id: lake-packages-cache
-        uses: actions/cache/restore@v5
-        with:
-          path: ${{ env.LAKE_PKG_DIR }}
-          key: lake-packages-${{ runner.os }}-${{ hashFiles('Lampe/lean-toolchain', 'Lampe/lake-manifest.json', 'stdlib/lampe/lean-toolchain', 'stdlib/lampe/lake-manifest.json') }}
+      - name: Point Lampe Lake Packages At Shared Dir
+        run: python3 scripts/ci/link_lake_packages.py Lampe
       - name: Restore Lampe Build Cache
-        id: lampe-build-cache
         uses: actions/cache@v5
         with:
           path: Lampe/.lake/build
-          key: lampe-build-${{ runner.os }}-${{ hashFiles('Lampe/**/*.lean', 'Lampe/**/*.toml', 'Lampe/**/*.json', 'Lampe/lean-toolchain', 'Lampe/lake-manifest.json', 'Lampe/lakefile.toml') }}
+          key: ${{ needs.keys.outputs.lampe_key }}
           restore-keys: |
             lampe-build-${{ runner.os }}-
       - name: Get Mathlib Cache
-        if: ${{ steps.lampe-build-cache.outputs.cache-hit != 'true' }}
         working-directory: Lampe
-        run: lake exe cache get
+        run: lake exe cache get || echo "cache get failed; continuing so the build step surfaces the real error"
       - name: Make All (Lampe)
-        if: ${{ steps.lampe-build-cache.outputs.cache-hit != 'true' }}
         working-directory: Lampe
         run: lake exe mk_all --check --lib Lampe
       - name: Build Lampe
-        if: ${{ steps.lampe-build-cache.outputs.cache-hit != 'true' }}
         working-directory: Lampe
         run: lake build
       - name: Test Lampe
-        if: ${{ steps.lampe-build-cache.outputs.cache-hit != 'true' }}
         working-directory: Lampe
         run: lake test
-      - name: Check Lake Packages Cache Contents
-        id: lake-packages-content
-        if: ${{ steps.lampe-build-cache.outputs.cache-hit != 'true' && steps.lake-packages-cache.outputs.cache-hit != 'true' }}
-        run: |
-          if [ -n "$(find "$LAKE_PKG_DIR" -mindepth 1 -print -quit)" ]; then
-            echo "has_files=true" >> "$GITHUB_OUTPUT"
-          else
-            echo "has_files=false" >> "$GITHUB_OUTPUT"
-          fi
-      - name: Save Lake Packages Cache
-        if: ${{ steps.lampe-build-cache.outputs.cache-hit != 'true' && steps.lake-packages-cache.outputs.cache-hit != 'true' && steps.lake-packages-content.outputs.has_files == 'true' }}
-        uses: actions/cache/save@v5
-        with:
-          path: ${{ env.LAKE_PKG_DIR }}
-          key: lake-packages-${{ runner.os }}-${{ hashFiles('Lampe/lean-toolchain', 'Lampe/lake-manifest.json', 'stdlib/lampe/lean-toolchain', 'stdlib/lampe/lake-manifest.json') }}
 
   build-stdlib:
     name: Build Stdlib
-    needs: [build-ci-image, build-rust, build-lean, ensure-noir-version]
+    needs: [build-ci-image, keys, build-rust, build-lean, ensure-noir-version]
+    if: ${{ !failure() && !cancelled() && needs.keys.outputs.stdlib_hit != 'true' }}
     runs-on: ubuntu-latest
-    env:
-      CI_IMAGE: ghcr.io/reilabs/lampe-ci:${{ needs.build-ci-image.outputs.image_tag }}
     container:
       image: ghcr.io/reilabs/lampe-ci:${{ needs.build-ci-image.outputs.image_tag }}
       credentials:
@@ -242,101 +275,36 @@ jobs:
         run: |
           mkdir -p "$RUNNER_TEMP/lake-packages"
           echo "LAKE_PKG_DIR=$RUNNER_TEMP/lake-packages" >> "$GITHUB_ENV"
-      - name: Restore Lake Packages Cache
-        id: lake-packages-cache
-        uses: actions/cache/restore@v5
-        with:
-          path: ${{ env.LAKE_PKG_DIR }}
-          key: lake-packages-${{ runner.os }}-${{ hashFiles('Lampe/lean-toolchain', 'Lampe/lake-manifest.json', 'stdlib/lampe/lean-toolchain', 'stdlib/lampe/lake-manifest.json') }}
       - name: Restore Lampe Build Cache
-        uses: actions/cache@v5
+        uses: actions/cache/restore@v5
         with:
           path: Lampe/.lake/build
-          key: lampe-build-${{ runner.os }}-${{ hashFiles('Lampe/**/*.lean', 'Lampe/**/*.toml', 'Lampe/**/*.json', 'Lampe/lean-toolchain', 'Lampe/lake-manifest.json', 'Lampe/lakefile.toml') }}
+          key: ${{ needs.keys.outputs.lampe_key }}
           restore-keys: |
             lampe-build-${{ runner.os }}-
       - name: Restore Stdlib Build Cache
-        id: stdlib-build-cache
         uses: actions/cache@v5
         with:
           path: stdlib/lampe/.lake/build
-          key: stdlib-build-${{ runner.os }}-${{ hashFiles('stdlib/src/**', 'stdlib/Nargo.toml', 'stdlib/test.xsh', 'stdlib/lampe/**/*.lean', 'stdlib/lampe/lean-toolchain', 'stdlib/lampe/lake-manifest.json', 'stdlib/lampe/lakefile.toml', 'Lampe/**/*.lean', 'Lampe/**/*.toml', 'Lampe/**/*.json', 'Lampe/lean-toolchain', 'Lampe/lake-manifest.json', 'Lampe/lakefile.toml', 'scripts/test.xsh', 'scripts/utils.xsh', 'Cargo.toml', 'Cargo.lock', 'rust-toolchain.toml', 'src/**') }}
+          key: ${{ needs.keys.outputs.stdlib_key }}
           restore-keys: |
             stdlib-build-${{ runner.os }}-
-      - name: Restore CLI Cache
-        id: cli-cache
-        uses: actions/cache@v5
-        with:
-          path: target/release/lampe
-          key: cli-${{ runner.os }}-${{ hashFiles('Cargo.toml', 'Cargo.lock', 'rust-toolchain.toml', 'src/**', 'Lampe/lean-toolchain') }}
-      - name: Check CLI Binary
-        id: cli-check
-        run: |
-          if [ -x target/release/lampe ]; then
-            echo "found=true" >> "$GITHUB_OUTPUT"
-          else
-            echo "found=false" >> "$GITHUB_OUTPUT"
-          fi
       - name: Download CLI Artifact
-        if: ${{ steps.cli-check.outputs.found != 'true' }}
-        continue-on-error: true
         uses: actions/download-artifact@v4
         with:
           name: lampe-cli-${{ github.sha }}
           path: target/release
-      - name: Re-check CLI Binary
-        id: cli-check-2
-        run: |
-          if [ -x target/release/lampe ]; then
-            echo "found=true" >> "$GITHUB_OUTPUT"
-          else
-            echo "found=false" >> "$GITHUB_OUTPUT"
-          fi
-      - name: Build CLI (Fallback)
-        if: ${{ steps.cli-check-2.outputs.found != 'true' }}
-        run: cargo build --release
       - name: Ensure CLI Executable
+        # upload-artifact zips files and drops the exec bit.
         run: chmod +x target/release/lampe
       - name: Test Stdlib Extraction
-        if: ${{ steps.stdlib-build-cache.outputs.cache-hit != 'true' }}
         run: ./stdlib/test.xsh
-      - name: Point Stdlib Lake Packages At Shared Cache
-        if: ${{ steps.stdlib-build-cache.outputs.cache-hit != 'true' }}
-        run: |
-          mkdir -p stdlib/lampe/.lake
-          rm -rf stdlib/lampe/.lake/packages
-          ln -s "$LAKE_PKG_DIR" stdlib/lampe/.lake/packages
-      - name: Free Runner Disk Space
-        if: ${{ steps.stdlib-build-cache.outputs.cache-hit != 'true' }}
-        uses: ./.github/actions/free-disk-space
-      - name: Build Stdlib In Place
-        if: ${{ steps.stdlib-build-cache.outputs.cache-hit != 'true' }}
-        run: |
-          cd stdlib/lampe
-          lake exe cache get
-          lake build
-      - name: Check Lake Packages Cache Contents
-        id: lake-packages-content
-        if: ${{ steps.stdlib-build-cache.outputs.cache-hit != 'true' && steps.lake-packages-cache.outputs.cache-hit != 'true' }}
-        run: |
-          if [ -n "$(find "$LAKE_PKG_DIR" -mindepth 1 -print -quit)" ]; then
-            echo "has_files=true" >> "$GITHUB_OUTPUT"
-          else
-            echo "has_files=false" >> "$GITHUB_OUTPUT"
-          fi
-      - name: Save Lake Packages Cache
-        if: ${{ steps.stdlib-build-cache.outputs.cache-hit != 'true' && steps.lake-packages-cache.outputs.cache-hit != 'true' && steps.lake-packages-content.outputs.has_files == 'true' }}
-        uses: actions/cache/save@v5
-        with:
-          path: ${{ env.LAKE_PKG_DIR }}
-          key: lake-packages-${{ runner.os }}-${{ hashFiles('Lampe/lean-toolchain', 'Lampe/lake-manifest.json', 'stdlib/lampe/lean-toolchain', 'stdlib/lampe/lake-manifest.json') }}
 
   end-to-end:
     name: E2E Tests
-    needs: [build-ci-image, build-rust, build-stdlib, build-lean, ensure-noir-version]
+    needs: [build-ci-image, keys, build-rust, build-stdlib, build-lean, ensure-noir-version]
+    if: ${{ !failure() && !cancelled() && needs.keys.outputs.e2e_hit != 'true' }}
     runs-on: ubuntu-latest
-    env:
-      CI_IMAGE: ghcr.io/reilabs/lampe-ci:${{ needs.build-ci-image.outputs.image_tag }}
     container:
       image: ghcr.io/reilabs/lampe-ci:${{ needs.build-ci-image.outputs.image_tag }}
       credentials:
@@ -349,78 +317,40 @@ jobs:
         run: |
           mkdir -p "$RUNNER_TEMP/lake-packages"
           echo "LAKE_PKG_DIR=$RUNNER_TEMP/lake-packages" >> "$GITHUB_ENV"
-      - name: Restore Lake Packages Cache
-        uses: actions/cache/restore@v5
-        with:
-          path: ${{ env.LAKE_PKG_DIR }}
-          key: lake-packages-${{ runner.os }}-${{ hashFiles('Lampe/lean-toolchain', 'Lampe/lake-manifest.json', 'stdlib/lampe/lean-toolchain', 'stdlib/lampe/lake-manifest.json') }}
       - name: Restore Lampe Build Cache
-        uses: actions/cache@v5
+        uses: actions/cache/restore@v5
         with:
           path: Lampe/.lake/build
-          key: lampe-build-${{ runner.os }}-${{ hashFiles('Lampe/**/*.lean', 'Lampe/**/*.toml', 'Lampe/**/*.json', 'Lampe/lean-toolchain', 'Lampe/lake-manifest.json', 'Lampe/lakefile.toml') }}
+          key: ${{ needs.keys.outputs.lampe_key }}
           restore-keys: |
             lampe-build-${{ runner.os }}-
       - name: Restore Stdlib Build Cache
         uses: actions/cache/restore@v5
         with:
           path: stdlib/lampe/.lake/build
-          key: stdlib-build-${{ runner.os }}-${{ hashFiles('stdlib/src/**', 'stdlib/Nargo.toml', 'stdlib/test.xsh', 'stdlib/lampe/**/*.lean', 'stdlib/lampe/lean-toolchain', 'stdlib/lampe/lake-manifest.json', 'stdlib/lampe/lakefile.toml', 'Lampe/**/*.lean', 'Lampe/**/*.toml', 'Lampe/**/*.json', 'Lampe/lean-toolchain', 'Lampe/lake-manifest.json', 'Lampe/lakefile.toml', 'scripts/test.xsh', 'scripts/utils.xsh', 'Cargo.toml', 'Cargo.lock', 'rust-toolchain.toml', 'src/**') }}
+          key: ${{ needs.keys.outputs.stdlib_key }}
           restore-keys: |
             stdlib-build-${{ runner.os }}-
       - name: Point Stdlib Lake Packages At Shared Cache
-        run: |
-          mkdir -p stdlib/lampe/.lake
-          rm -rf stdlib/lampe/.lake/packages
-          ln -s "$LAKE_PKG_DIR" stdlib/lampe/.lake/packages
-      - name: Restore CLI Cache
-        id: cli-cache
-        uses: actions/cache@v5
-        with:
-          path: target/release/lampe
-          key: cli-${{ runner.os }}-${{ hashFiles('Cargo.toml', 'Cargo.lock', 'rust-toolchain.toml', 'src/**', 'Lampe/lean-toolchain') }}
-      - name: Check CLI Binary
-        id: cli-check
-        run: |
-          if [ -x target/release/lampe ]; then
-            echo "found=true" >> "$GITHUB_OUTPUT"
-          else
-            echo "found=false" >> "$GITHUB_OUTPUT"
-          fi
+        run: python3 scripts/ci/link_lake_packages.py stdlib/lampe
       - name: Download CLI Artifact
-        if: ${{ steps.cli-check.outputs.found != 'true' }}
-        continue-on-error: true
         uses: actions/download-artifact@v4
         with:
           name: lampe-cli-${{ github.sha }}
           path: target/release
-      - name: Re-check CLI Binary
-        id: cli-check-2
-        run: |
-          if [ -x target/release/lampe ]; then
-            echo "found=true" >> "$GITHUB_OUTPUT"
-          else
-            echo "found=false" >> "$GITHUB_OUTPUT"
-          fi
-      - name: Build CLI (Fallback)
-        if: ${{ steps.cli-check-2.outputs.found != 'true' }}
-        run: cargo build --release
       - name: Ensure CLI Executable
+        # upload-artifact zips files and drops the exec bit.
         run: chmod +x target/release/lampe
-      - name: Restore E2E Cache
-        id: e2e-cache
-        uses: actions/cache@v5
-        with:
-          path: .ci-cache/e2e
-          key: e2e-${{ runner.os }}-${{ hashFiles('testing/**', 'scripts/test.xsh', 'scripts/utils.xsh', 'Cargo.toml', 'Cargo.lock', 'rust-toolchain.toml', 'src/**', 'Lampe/**/*.lean', 'Lampe/**/*.toml', 'Lampe/**/*.json', 'Lampe/lean-toolchain', 'Lampe/lake-manifest.json', 'Lampe/lakefile.toml', 'stdlib/src/**', 'stdlib/Nargo.toml', 'stdlib/lampe/**/*.lean', 'stdlib/lampe/lean-toolchain', 'stdlib/lampe/lake-manifest.json', 'stdlib/lampe/lakefile.toml') }}
       - name: Free Runner Disk Space
-        if: ${{ steps.e2e-cache.outputs.cache-hit != 'true' }}
         uses: ./.github/actions/free-disk-space
       - name: Run Test Script
-        if: ${{ steps.e2e-cache.outputs.cache-hit != 'true' }}
         run: ./testing/test.xsh
       - name: Mark E2E Cache
-        if: ${{ steps.e2e-cache.outputs.cache-hit != 'true' }}
         run: |
           mkdir -p .ci-cache/e2e
           echo "ok" > .ci-cache/e2e/success
+      - name: Save E2E Cache
+        uses: actions/cache/save@v5
+        with:
+          path: .ci-cache/e2e
+          key: ${{ needs.keys.outputs.e2e_key }}

From 60542d435064f10d0ca4945459c7287c75754b3e Mon Sep 17 00:00:00 2001
From: Eduardo Gomes <eduardogbg@gmail.com>
Date: Thu, 11 Jun 2026 16:17:29 -0300
Subject: [PATCH 7/8] ci: cancel superseded PR runs with a per-ref concurrency
 group

---
 .github/workflows/ci.yaml | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml
index 70d5be4e..07ecb38c 100644
--- a/.github/workflows/ci.yaml
+++ b/.github/workflows/ci.yaml
@@ -6,6 +6,13 @@ on:
   pull_request:
   workflow_dispatch:
 
+# One run per ref: a new push cancels the previous in-flight PR run instead
+# of racing it (two parallel runs would each build and push the same image
+# tag). Runs on main are never cancelled.
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: ${{ github.event_name == 'pull_request' }}
+
 permissions:
   contents: read
   packages: write

From e217351a50e9c86d8abbd8187925c8bfc1256532 Mon Sep 17 00:00:00 2001
From: Eduardo Gomes <eduardogbg@gmail.com>
Date: Fri, 12 Jun 2026 00:25:24 -0300
Subject: [PATCH 8/8] ci: add a gate job reporting the required Build CI Image
 check

---
 .github/workflows/build-ci-image.yaml | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/.github/workflows/build-ci-image.yaml b/.github/workflows/build-ci-image.yaml
index 00733ccc..e3ae376d 100644
--- a/.github/workflows/build-ci-image.yaml
+++ b/.github/workflows/build-ci-image.yaml
@@ -92,3 +92,15 @@ jobs:
         run: |
           echo "CI image ghcr.io/reilabs/lampe-ci:${{ needs.check.outputs.image_tag }} is missing and cannot be built from a fork."
           exit 1
+
+  # Branch protection requires a check named "build-ci-image / Build CI Image";
+  # this job reports that context and fails if any of the jobs above failed.
+  gate:
+    name: Build CI Image
+    needs: [check, build, guard]
+    if: always()
+    runs-on: ubuntu-latest
+    steps:
+      - name: Check Job Results
+        run: |
+          [ "${{ contains(needs.*.result, 'failure') || contains(needs.*.result, 'cancelled') }}" != "true" ]