From 1b98e5db274352dbdc2dff2725d38f7fc178013a Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 26 Oct 2026 23:01:11 +0000 Subject: [PATCH 1/3] ci(kernel-proofs): pin the runner and require Agda 2.6.3 ubuntu-latest moved to Ubuntu 26.04 on 2026-10-19. The kernel-proofs job installs Agda from apt, so it got Agda 2.8.0, which prints error locations as file:11.38 where 2.6.3 printed file:11,38. occupancy-types' own reject check only accepts the old form, so it reported CostIsOccupancy as an unexpected failure even though Agda refused it correctly. Every PR now fails the job; main last ran it on 2026-10-17, before the move. The job runs on ubuntu-24.04, whose agda-bin is 2.6.3, and check-kernel-proofs.sh refuses any other Agda (ALLOW_ANY_AGDA=1 to override), as it already refuses any Idris2 but 0.8.0. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t --- .github/workflows/contract-gate.yml | 6 +++++- CHANGELOG.adoc | 12 ++++++++++++ tools/check-kernel-proofs.sh | 7 +++++++ 3 files changed, 24 insertions(+), 1 deletion(-) diff --git a/.github/workflows/contract-gate.yml b/.github/workflows/contract-gate.yml index 41157d6..7d27b61 100644 --- a/.github/workflows/contract-gate.yml +++ b/.github/workflows/contract-gate.yml @@ -56,7 +56,11 @@ jobs: # cannot). kernel-proofs: name: Grade kernel proofs (Idris2 0.8.0 + Agda) - runs-on: ubuntu-latest + # Pinned: the job installs Agda from apt, so the image decides the Agda + # version, and the reject checks need 2.6.3 (tools/check-kernel-proofs.sh + # refuses any other). ubuntu-latest moved to 26.04 (Agda 2.8.0) on + # 2026-10-19. + runs-on: ubuntu-24.04 timeout-minutes: 40 env: IDRIS2_COMMIT: 15a3e4e70843f7a34100f6470c04b791330788df # v0.8.0 diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index 834cca1..dbff89f 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -9,6 +9,18 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning]. === [Unreleased] +==== Kernel proofs pinned to Agda 2.6.3 (2026-10-26) + +* `ubuntu-latest` moved to Ubuntu 26.04 on 2026-10-19, so the Contract + Gate's kernel-proofs job, which installs Agda from apt, got Agda 2.8.0. + 2.8.0 prints error locations as `file:11.38` where 2.6.3 printed + `file:11,38`, and occupancy-types' own reject check accepts only the old + form, so it reported `CostIsOccupancy` as an unexpected failure although + Agda refused it correctly. +* The job now runs on `ubuntu-24.04`, whose `agda-bin` is 2.6.3, and + `tools/check-kernel-proofs.sh` refuses any other Agda (as it already + refuses any Idris2 but 0.8.0), unless `ALLOW_ANY_AGDA=1` is set. + ==== occupancy-types pin `6013483` → `8f09c0b` (2026-10-14) * `scripts/fetch-siblings.sh` pins occupancy-types at `8f09c0b`, the merge of diff --git a/tools/check-kernel-proofs.sh b/tools/check-kernel-proofs.sh index 8f5757e..e005cfa 100755 --- a/tools/check-kernel-proofs.sh +++ b/tools/check-kernel-proofs.sh @@ -48,6 +48,13 @@ case "$iv" in *"version 0.8.0"*) ;; *) [ -n "${ALLOW_ANY_IDRIS2:-}" ] || die "Idris2 0.8.0 required (src/abi targets 0.8.0; EXPECT messages are 0.8.0's). Set ALLOW_ANY_IDRIS2=1 to try another." ;; esac +# The rejection checks match prover messages and locations, and both change +# between Agda releases: 2.8.0 prints `file:11.38` where 2.6.3 printed +# `file:11,38`, which occupancy-types' own reject check does not accept. +case "$av" in + *"version 2.6.3"*) ;; + *) [ -n "${ALLOW_ANY_AGDA:-}" ] || die "Agda 2.6.3 required (the pinned siblings' reject checks expect 2.6.3's messages). Set ALLOW_ANY_AGDA=1 to try another." ;; +esac [ -d "$RA/src/ResourceAlgebra" ] || die "resource-algebra not fetched — run scripts/fetch-siblings.sh" echo "resource-algebra at $(git -C "$RA" rev-parse HEAD)" rm -rf "$OUT"; mkdir -p "$OUT" From 1e4944afefdbd9d13a7d003a56b3856d75807203 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 26 Oct 2026 23:04:56 +0000 Subject: [PATCH 2/3] ci(kernel-proofs): use [[ ]] in the Agda version check SonarCloud (shell rule: prefer [[ over [) on the line added in 1b98e5d. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t --- tools/check-kernel-proofs.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tools/check-kernel-proofs.sh b/tools/check-kernel-proofs.sh index e005cfa..a5aec39 100755 --- a/tools/check-kernel-proofs.sh +++ b/tools/check-kernel-proofs.sh @@ -53,7 +53,7 @@ esac # `file:11,38`, which occupancy-types' own reject check does not accept. case "$av" in *"version 2.6.3"*) ;; - *) [ -n "${ALLOW_ANY_AGDA:-}" ] || die "Agda 2.6.3 required (the pinned siblings' reject checks expect 2.6.3's messages). Set ALLOW_ANY_AGDA=1 to try another." ;; + *) [[ -n "${ALLOW_ANY_AGDA:-}" ]] || die "Agda 2.6.3 required (the pinned siblings' reject checks expect 2.6.3's messages). Set ALLOW_ANY_AGDA=1 to try another." ;; esac [ -d "$RA/src/ResourceAlgebra" ] || die "resource-algebra not fetched — run scripts/fetch-siblings.sh" echo "resource-algebra at $(git -C "$RA" rev-parse HEAD)" From af65bba9780a271729f1dca33daa82c0b3d2dbd7 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 26 Oct 2026 23:10:10 +0000 Subject: [PATCH 3/3] ci(kernel-proofs): match the whole Agda version line The glob *"version 2.6.3"* also accepted 2.6.3.1 or 2.6.30. The check now requires the line to be exactly "Agda version 2.6.3". Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t --- tools/check-kernel-proofs.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tools/check-kernel-proofs.sh b/tools/check-kernel-proofs.sh index a5aec39..043c403 100755 --- a/tools/check-kernel-proofs.sh +++ b/tools/check-kernel-proofs.sh @@ -52,7 +52,7 @@ esac # between Agda releases: 2.8.0 prints `file:11.38` where 2.6.3 printed # `file:11,38`, which occupancy-types' own reject check does not accept. case "$av" in - *"version 2.6.3"*) ;; + "Agda version 2.6.3") ;; # the whole line: 2.6.3.1 is another release *) [[ -n "${ALLOW_ANY_AGDA:-}" ]] || die "Agda 2.6.3 required (the pinned siblings' reject checks expect 2.6.3's messages). Set ALLOW_ANY_AGDA=1 to try another." ;; esac [ -d "$RA/src/ResourceAlgebra" ] || die "resource-algebra not fetched — run scripts/fetch-siblings.sh"