From dd11703e5ca72a1a590fffba969ef43b49980ca3 Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Mon, 19 Oct 2026 12:10:26 +0000
Subject: [PATCH] fix(ci): key the Idris 2 cache on the Chez Scheme version

`ubuntu-latest` moved to the 26.04 image. The cached ~/.idris2 holds an
idris2.so compiled by the previous image's Chez, and a fasl-object only
loads under the Chez that wrote it, so every cache hit now dies with

  Exception: incompatible fasl-object version 0.0.0-pre-release.73
  found in /home/runner/.idris2/bin/idris2_app/idris2.so

and abi-codegen-drift (a required check) is red on every PR. The cache key
did not name Chez, so the stale build kept being restored.

The installed chezscheme package version is now part of the key in both
workflows that share the entry (abi-codegen-drift.yml, verify-proofs.yml),
so an image or package change rebuilds Idris 2 once instead of loading a
stale build. verify-proofs.yml has the same latent failure; it simply has
not run on the new image yet.

Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_0165rGu3tsKmJtevmrdMVyfJ
---
 .github/workflows/abi-codegen-drift.yml | 19 ++++++++++++++++++-
 .github/workflows/verify-proofs.yml     | 19 ++++++++++++++++++-
 2 files changed, 36 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/abi-codegen-drift.yml b/.github/workflows/abi-codegen-drift.yml
index 0a436791..152de519 100644
--- a/.github/workflows/abi-codegen-drift.yml
+++ b/.github/workflows/abi-codegen-drift.yml
@@ -49,6 +49,23 @@ jobs:
           sudo apt-get update
           sudo apt-get install -y chezscheme
 
+      # The cached ~/.idris2 holds a Chez-compiled idris2.so. A fasl-object
+      # is only loadable by the Chez that wrote it, and `ubuntu-latest` moved
+      # to a newer image (26.04) with a newer Chez, so the old cache restored
+      # an idris2.so the new Chez refuses:
+      #   Exception: incompatible fasl-object version 0.0.0-pre-release.73
+      # The installed chezscheme package version is therefore part of the key,
+      # so an image or package bump rebuilds Idris 2 instead of loading a stale
+      # build. Keep this step and the key in step with abi-codegen-drift.yml /
+      # verify-proofs.yml, which share one cache entry on purpose.
+      - name: Chez Scheme version (Idris 2 cache key)
+        id: chez
+        run: |
+          set -euo pipefail
+          v="$(dpkg-query -W -f='${Version}' chezscheme | tr -c 'A-Za-z0-9.' '-')"
+          [ -n "$v" ]
+          echo "version=$v" >> "$GITHUB_OUTPUT"
+
       - name: Cache Idris 2 install
         id: cache-idris
         uses: actions/cache@v6.1.0
@@ -60,7 +77,7 @@ jobs:
           # bootstrap. Keep the suffix in step with it. `-3` = the
           # single-prefix layout (#820); `-2` and earlier entries are the
           # split-prefix caches and must not be restored.
-          key: idris2-${{ env.IDRIS2_VERSION }}-${{ runner.os }}-3
+          key: idris2-${{ env.IDRIS2_VERSION }}-${{ runner.os }}-chez${{ steps.chez.outputs.version }}-3
 
       - name: Build Idris 2 from source
         if: steps.cache-idris.outputs.cache-hit != 'true'
diff --git a/.github/workflows/verify-proofs.yml b/.github/workflows/verify-proofs.yml
index b61a34c6..e2131ad0 100644
--- a/.github/workflows/verify-proofs.yml
+++ b/.github/workflows/verify-proofs.yml
@@ -89,6 +89,23 @@ jobs:
           sudo apt-get update
           sudo apt-get install -y chezscheme
 
+      # The cached ~/.idris2 holds a Chez-compiled idris2.so. A fasl-object
+      # is only loadable by the Chez that wrote it, and `ubuntu-latest` moved
+      # to a newer image (26.04) with a newer Chez, so the old cache restored
+      # an idris2.so the new Chez refuses:
+      #   Exception: incompatible fasl-object version 0.0.0-pre-release.73
+      # The installed chezscheme package version is therefore part of the key,
+      # so an image or package bump rebuilds Idris 2 instead of loading a stale
+      # build. Keep this step and the key in step with abi-codegen-drift.yml /
+      # verify-proofs.yml, which share one cache entry on purpose.
+      - name: Chez Scheme version (Idris 2 cache key)
+        id: chez
+        run: |
+          set -euo pipefail
+          v="$(dpkg-query -W -f='${Version}' chezscheme | tr -c 'A-Za-z0-9.' '-')"
+          [ -n "$v" ]
+          echo "version=$v" >> "$GITHUB_OUTPUT"
+
       - name: Cache Idris 2 install
         id: cache-idris
         uses: actions/cache@v6.1.0
@@ -105,7 +122,7 @@ jobs:
           # every cache *hit* restored a launcher with no image and died
           # with `idris2_app/idris2.so: not found` (exit 127) before any
           # proof ran. ~/.idris2/bin/{idris2,idris2_app} travels together.
-          key: idris2-${{ env.IDRIS2_VERSION }}-${{ runner.os }}-3
+          key: idris2-${{ env.IDRIS2_VERSION }}-${{ runner.os }}-chez${{ steps.chez.outputs.version }}-3
 
       - name: Build Idris 2 from source
         if: steps.cache-idris.outputs.cache-hit != 'true'