Test !bench cslib

.github/workflows/build-post.yml

@@ -37,12 +37,12 @@ jobs:
         env:
           LAKE_CACHE_KEY: ${{ secrets.LAKE_CACHE_KEY }}
         run: |
-          TOOLCHAIN="$(cat "$RUNNER_TEMP/staging/lean-toolchain")"
-          TOOLCHAIN="${TOOLCHAIN#leanprover/lean4:}"
+          REV="$(cat "$RUNNER_TEMP/staging/.metadata/rev")"
+          TOOLCHAIN="$(cat "$RUNNER_TEMP/staging/.metadata/lean-toolchain")"
           .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

.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"
@@ -57,8 +56,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"
@@ -78,6 +78,7 @@ jobs:
         with:
           name: build-staging
           path: ${{ runner.temp }}/staging/
+          include-hidden-files: true
 
       - name: Fail if critical repos are not green
         run: |

.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

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!