From 9e96e08a7a100e3e837f339894d46bee3d057201 Mon Sep 17 00:00:00 2001
From: Joscha <joscha@plugh.de>
Date: Thu, 30 Jul 2026 16:43:28 +0200
Subject: [PATCH 1/4] ci: upload cache for correct sha

---
 .github/workflows/build-post.yml | 5 +++--
 .github/workflows/build.yml      | 5 +++--
 2 files changed, 6 insertions(+), 4 deletions(-)

diff --git a/.github/workflows/build-post.yml b/.github/workflows/build-post.yml
index a5ac69369..05e15d0a4 100644
--- a/.github/workflows/build-post.yml
+++ b/.github/workflows/build-post.yml
@@ -37,12 +37,13 @@ jobs:
         env:
           LAKE_CACHE_KEY: ${{ secrets.LAKE_CACHE_KEY }}
         run: |
-          TOOLCHAIN="$(cat "$RUNNER_TEMP/staging/lean-toolchain")"
+          REV="$(cat "$RUNNER_TEMP/staging/.metadata/rev")"
+          TOOLCHAIN="$(cat "$RUNNER_TEMP/staging/.metadata/lean-toolchain")"
           TOOLCHAIN="${TOOLCHAIN#leanprover/lean4:}"
           .downstream/list.py . | while IFS= read -r repo; do
             echo "::group::cache put-staged $repo"
             pushd "$repo"
-            lake cache put-staged "$RUNNER_TEMP/staging/$repo" --scope "$TOOLCHAIN/$repo" || true
+            lake cache put-staged "$RUNNER_TEMP/staging/$repo" --rev "$REV" --scope "$TOOLCHAIN/$repo" || true
             popd
             echo "::endgroup::"
           done
diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index c99ee57ef..ffda198dd 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -57,8 +57,9 @@ jobs:
 
       - name: Stage cache
         run: |
-          mkdir -p "$RUNNER_TEMP/staging"
-          cp lean-toolchain "$RUNNER_TEMP/staging/"
+          mkdir -p "$RUNNER_TEMP/staging/.metadata"
+          git rev-parse HEAD > "$RUNNER_TEMP/staging/.metadata/rev"
+          cp lean-toolchain "$RUNNER_TEMP/staging/.metadata/lean-toolchain"
           .downstream/list.py . | while IFS= read -r repo; do
             echo "::group::stage $repo"
             pushd "$repo"

From d3866a4516b09a69b5601f064f9fb6664792e608 Mon Sep 17 00:00:00 2001
From: Joscha <joscha@plugh.de>
Date: Thu, 30 Jul 2026 17:41:17 +0200
Subject: [PATCH 2/4] ci: fix staging metadata not being uploaded

---
 .github/workflows/build.yml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index ffda198dd..1d30d5b01 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -79,6 +79,7 @@ jobs:
         with:
           name: build-staging
           path: ${{ runner.temp }}/staging/
+          include-hidden-files: true
 
       - name: Fail if critical repos are not green
         run: |

From 433d5334dfd9b345f2d5cb4d7bab996f0e024397 Mon Sep 17 00:00:00 2001
From: Joscha <joscha@plugh.de>
Date: Thu, 30 Jul 2026 16:57:56 +0200
Subject: [PATCH 3/4] ci: always use full toolchain for cache scope

---
 .github/workflows/build-post.yml | 1 -
 .github/workflows/build.yml      | 1 -
 .meta/get-cache.sh               | 2 --
 3 files changed, 4 deletions(-)

diff --git a/.github/workflows/build-post.yml b/.github/workflows/build-post.yml
index 05e15d0a4..7917af5a9 100644
--- a/.github/workflows/build-post.yml
+++ b/.github/workflows/build-post.yml
@@ -39,7 +39,6 @@ jobs:
         run: |
           REV="$(cat "$RUNNER_TEMP/staging/.metadata/rev")"
           TOOLCHAIN="$(cat "$RUNNER_TEMP/staging/.metadata/lean-toolchain")"
-          TOOLCHAIN="${TOOLCHAIN#leanprover/lean4:}"
           .downstream/list.py . | while IFS= read -r repo; do
             echo "::group::cache put-staged $repo"
             pushd "$repo"
diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index 1d30d5b01..de7259705 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -31,7 +31,6 @@ jobs:
       - name: Restore cache
         run: |
           TOOLCHAIN="$(cat lean-toolchain)"
-          TOOLCHAIN="${TOOLCHAIN#leanprover/lean4:}"
           .downstream/list.py . | while IFS= read -r repo; do
             echo "::group::get $repo"
             pushd "$repo"
diff --git a/.meta/get-cache.sh b/.meta/get-cache.sh
index 9b2c017bd..5a2c8d759 100755
--- a/.meta/get-cache.sh
+++ b/.meta/get-cache.sh
@@ -5,8 +5,6 @@ ROOT_DIR=$(dirname "$META_DIR")
 export LAKE_CONFIG="$META_DIR/lake-config.toml"
 
 TOOLCHAIN="$(cat "$ROOT_DIR/lean-toolchain")"
-TOOLCHAIN="${TOOLCHAIN#leanprover/lean4:}"
-
 "$ROOT_DIR/.downstream/list.py" "$ROOT_DIR" -d -- "$@" | while IFS= read -r repo; do
   pushd "$ROOT_DIR/$repo"
   lake cache get --scope "$TOOLCHAIN/$repo" || true

From 225d321bff55dce1cc423d46f4d1ad22c08538b0 Mon Sep 17 00:00:00 2001
From: Joscha <joscha@plugh.de>
Date: Tue, 28 Jul 2026 22:22:52 +0200
Subject: [PATCH 4/4] bing bong

---
 README.md | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/README.md b/README.md
index debf2d5ea..98dd4b976 100644
--- a/README.md
+++ b/README.md
@@ -100,3 +100,5 @@ up-to-date, else our copy of your repo will receive no updates either.
 
 If you have any questions or concerns, please open an issue or contact Joscha
 Mennicken on the [community zulip](https://leanprover.zulipchat.com/).
+
+Bleep bloop!