From 99d53fe548d9009871511aa243a4ed6489cb735f Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 13 Oct 2026 23:59:22 +0000 Subject: [PATCH 1/2] fix(abi): CodeRabbit follow-ups from #149; agda-proofs is no longer DESIGNED Two CodeRabbit findings on #149 (merged before they could ride it), plus one stale status line: - ffi/zig/include/januskey.h: the header said Foreign.idr is "checked by the ABI package typecheck". The typecheck does not compare the two files. On this stack the comparison is scripts/check-abi-layout.sh (symbols, status codes, enums, sizes; ledger row A-3), and the comment now names it. - scripts/check-abi-tree.sh: a dangling symlink at src/idris-abi passed `[ -e ]`, so the retired farm could come back as a broken link unnoticed. The check is now `-e || -L`. Reproduced: with `ln -s does-not-exist src/idris-abi` the old gate exits 0 and the new one exits 1 with "src/idris-abi exists (retired symlink farm)". - .github/workflows/agda-proofs.yml: "DESIGNED until its first green run" is no longer true; its first run on #150 was green under Agda 2.6.4.3 with both fixtures refused for their stated reasons. Checks: check-abi-tree OK, check-abi-layout PASS, workflow YAML parses. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Kjdf4Mf4Z41bNQh2TrsEp9 --- .github/workflows/agda-proofs.yml | 2 +- ffi/zig/include/januskey.h | 2 +- scripts/check-abi-tree.sh | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/.github/workflows/agda-proofs.yml b/.github/workflows/agda-proofs.yml index 2f53eef..5e13504 100644 --- a/.github/workflows/agda-proofs.yml +++ b/.github/workflows/agda-proofs.yml @@ -1,7 +1,7 @@ # SPDX-License-Identifier: MPL-2.0 # SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell name: Agda proofs -# DESIGNED until its first green run. Pattern: choreographic-types / +# First green run 2026-10-13, Agda 2.6.4.3 (PR #150). Pattern: choreographic-types / # residual-evidence-types (pinned Debian prover, sibling fetched by commit). # Checks verification/proofs/agda/Reversibility.agda under the kernel flags # and refuses the fixtures under tests/reject-agda. Local run: just test-agda. diff --git a/ffi/zig/include/januskey.h b/ffi/zig/include/januskey.h index 18c595f..e548ac6 100644 --- a/ffi/zig/include/januskey.h +++ b/ffi/zig/include/januskey.h @@ -2,7 +2,7 @@ // Copyright (c) Jonathan D.A. Jewell /* SPDX-License-Identifier: MPL-2.0 */ /* Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) */ -/* JanusKey C FFI Header — hand-maintained; src/abi/JanusKey/ABI/Foreign.idr must mirror it (checked by the ABI package typecheck) */ +/* JanusKey C FFI Header — hand-maintained; src/abi/JanusKey/ABI/Foreign.idr mirrors it: symbols, status codes, enums and sizes are compared by scripts/check-abi-layout.sh */ #ifndef JANUSKEY_H #define JANUSKEY_H diff --git a/scripts/check-abi-tree.sh b/scripts/check-abi-tree.sh index 923e761..76b3f16 100755 --- a/scripts/check-abi-tree.sh +++ b/scripts/check-abi-tree.sh @@ -10,7 +10,7 @@ fail=0 say() { echo "[check-abi-tree] $*"; } # 1. The symlink farm (PR #140, src/idris-abi/) is retired. -if [ -e src/idris-abi ]; then say "FAIL: src/idris-abi exists (retired symlink farm)"; fail=1; fi +if [ -e src/idris-abi ] || [ -L src/idris-abi ]; then say "FAIL: src/idris-abi exists (retired symlink farm)"; fail=1; fi # 2. Exactly one package file, and it is the one the gates name. n=$(find src/abi -name '*.ipkg' | wc -l) From 96f7804d67817b409e1aed8363a39c65a63bb553 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 14 Oct 2026 00:01:40 +0000 Subject: [PATCH 2/2] ci(proofs): give the Agda job a timeout (Hypatia WH006 on #150) Hypatia flagged two warnings on #150, both for the same thing: job `proofs` in agda-proofs.yml had no `timeout-minutes`, so a hung apt install or sibling fetch could hold a runner for the 360-minute default. The job takes about 35 s; 15 minutes matches idris-abi.yml. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Kjdf4Mf4Z41bNQh2TrsEp9 --- .github/workflows/agda-proofs.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/.github/workflows/agda-proofs.yml b/.github/workflows/agda-proofs.yml index 5e13504..4399a3c 100644 --- a/.github/workflows/agda-proofs.yml +++ b/.github/workflows/agda-proofs.yml @@ -15,6 +15,7 @@ jobs: proofs: name: Reversibility as a grade (Loss instance), expected rejections runs-on: ubuntu-latest + timeout-minutes: 15 # trixie-slim, resolved 2026-10-13; re-pin deliberately, like the prover below. container: debian:trixie-slim@sha256:a29215f6a35e51e22adffa17f89e9d2ef06214e64a2bad10d765c46aea49f11f steps: