Skip to content

ci(kernel-proofs): pin the runner and require Agda 2.6.3 #280

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
hyperpolymath merged 3 commits into from
Oct 27, 2026
Merged

ci(kernel-proofs): pin the runner and require Agda 2.6.3 #280

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
1b98e5d
ci(kernel-proofs): pin the runner and require Agda 2.6.3
claude Oct 26, 2026
1e4944a
ci(kernel-proofs): use [[ ]] in the Agda version check
claude Oct 26, 2026
af65bba
ci(kernel-proofs): match the whole Agda version line
claude Oct 26, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 5 additions & 1 deletion .github/workflows/contract-gate.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
12 changes: 12 additions & 0 deletions CHANGELOG.adoc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
7 changes: 7 additions & 0 deletions tools/check-kernel-proofs.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
"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"
echo "resource-algebra at $(git -C "$RA" rev-parse HEAD)"
rm -rf "$OUT"; mkdir -p "$OUT"
Expand Down
Loading