From a6227af43b07a31b648b848f9fc0124e33c735f5 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Fri, 2 Oct 2026 13:09:03 +0100 Subject: [PATCH] fix(test-proofs): make the Idris2 ABI check able to fail The old `test-proofs` recipe could never fail: it used `$$f` (bash saw PID+"f", so every file was reported [SKIP]), a failing `idris2 --check` only printed [FAIL], and a missing idris2 exited 0. - Add src/idris-abi/januskey-abi.ipkg. Idris2 resolves A.B.C to /A/B/C.idr, and the ABI sources sit flat in src/abi/, so no sourcedir can reach them. They are not moved (aspect tests, Mustfile and the Zig FFI name src/abi/.idr); instead src/idris-abi/ holds relative symlinks laid out by declared module name. Foreign.idr's `Januskey.ABI.Foreign` casing is listed as declared and left for J1-3. - Rewrite `test-proofs` as a bash shebang recipe with `set -euo pipefail` running `idris2 --typecheck` on the package. Missing idris2 exits 1 unless ALLOW_NO_IDRIS=1, which exits 0 with a loud SKIP. - Add the non-required workflow job "idris-abi (expected red until J1-3)" running the same typecheck in the idris2-pack image already used by pages.yml. Expected: `just test-proofs` now exits 1 on the known Types.idr errors. Co-Authored-By: Claude Opus 5.5 --- .github/workflows/idris-abi.yml | 28 ++++++++++++++++++++++++ Justfile | 29 ++++++++++++++----------- src/idris-abi/JanusKey/ABI/Layout.idr | 1 + src/idris-abi/JanusKey/ABI/Proofs.idr | 1 + src/idris-abi/JanusKey/ABI/Types.idr | 1 + src/idris-abi/Januskey/ABI/Foreign.idr | 1 + src/idris-abi/januskey-abi.ipkg | 30 ++++++++++++++++++++++++++ 7 files changed, 78 insertions(+), 13 deletions(-) create mode 100644 .github/workflows/idris-abi.yml create mode 120000 src/idris-abi/JanusKey/ABI/Layout.idr create mode 120000 src/idris-abi/JanusKey/ABI/Proofs.idr create mode 120000 src/idris-abi/JanusKey/ABI/Types.idr create mode 120000 src/idris-abi/Januskey/ABI/Foreign.idr create mode 100644 src/idris-abi/januskey-abi.ipkg diff --git a/.github/workflows/idris-abi.yml b/.github/workflows/idris-abi.yml new file mode 100644 index 0000000..04cb957 --- /dev/null +++ b/.github/workflows/idris-abi.yml @@ -0,0 +1,28 @@ +# SPDX-License-Identifier: MPL-2.0 +# Typechecks the Idris2 ABI package (src/idris-abi/januskey-abi.ipkg). +# NOT a required check: it is expected to be red until J1-3 fixes the known +# errors in src/abi (Types.idr, and the Januskey/JanusKey module-name casing). +name: Idris ABI typecheck +on: + pull_request: + push: + branches: [main] + workflow_dispatch: +permissions: + contents: read +jobs: + idris-abi: + name: "idris-abi (expected red until J1-3)" + runs-on: ubuntu-latest + timeout-minutes: 15 + container: + image: ghcr.io/stefan-hoeck/idris2-pack@sha256:f0758996a931fb35d9ecb1de273c4d59dabe2a09b433afc7e357f65a08b7e1ff + steps: + - name: Checkout + uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + with: + persist-credentials: false + - name: Typecheck ABI package + run: | + idris2 --version + idris2 --typecheck src/idris-abi/januskey-abi.ipkg diff --git a/Justfile b/Justfile index 506c540..44b485a 100644 --- a/Justfile +++ b/Justfile @@ -88,21 +88,24 @@ test-contracts: done; \ fi -# Check Idris2 ABI proofs (requires idris2) +# Typecheck the Idris2 ABI package (src/idris-abi/januskey-abi.ipkg). +# Fails if idris2 is missing (set ALLOW_NO_IDRIS=1 to skip) or any module fails. test-proofs: - @echo "=== Proof Regression ===" - @if command -v idris2 >/dev/null 2>&1; then \ - for f in src/abi/Types.idr src/abi/Layout.idr src/abi/Foreign.idr src/abi/Proofs.idr; do \ - if [ -f "$$f" ]; then \ - echo "Checking $$f..."; \ - idris2 --check "$$f" && echo " [OK] $$f" || echo " [FAIL] $$f"; \ - else \ - echo " [SKIP] $$f not found"; \ - fi; \ - done; \ - else \ - echo "SKIP: idris2 not installed. Install via: pack install-app idris2"; \ + #!/usr/bin/env bash + set -euo pipefail + echo "=== Proof Regression ===" + ipkg="src/idris-abi/januskey-abi.ipkg" + if ! command -v idris2 >/dev/null 2>&1; then + if [ "${ALLOW_NO_IDRIS:-0}" = "1" ]; then + echo "SKIP: idris2 not installed and ALLOW_NO_IDRIS=1 -- ABI proofs were NOT checked." >&2 + exit 0 + fi + echo "FAIL: idris2 not installed; cannot check ABI proofs. Install via: pack install-app idris2 (or set ALLOW_NO_IDRIS=1 to skip explicitly)." >&2 + exit 1 fi + echo "idris2 --typecheck $ipkg ($(idris2 --version))" + idris2 --typecheck "$ipkg" + echo "[OK] ABI package typechecks" # Run full test suite (all categories) test-all: test test-p2p test-regressions test-e2e test-aspect test-contracts test-proofs smoke diff --git a/src/idris-abi/JanusKey/ABI/Layout.idr b/src/idris-abi/JanusKey/ABI/Layout.idr new file mode 120000 index 0000000..fd00422 --- /dev/null +++ b/src/idris-abi/JanusKey/ABI/Layout.idr @@ -0,0 +1 @@ +../../../abi/Layout.idr \ No newline at end of file diff --git a/src/idris-abi/JanusKey/ABI/Proofs.idr b/src/idris-abi/JanusKey/ABI/Proofs.idr new file mode 120000 index 0000000..d63c148 --- /dev/null +++ b/src/idris-abi/JanusKey/ABI/Proofs.idr @@ -0,0 +1 @@ +../../../abi/Proofs.idr \ No newline at end of file diff --git a/src/idris-abi/JanusKey/ABI/Types.idr b/src/idris-abi/JanusKey/ABI/Types.idr new file mode 120000 index 0000000..2c77c1f --- /dev/null +++ b/src/idris-abi/JanusKey/ABI/Types.idr @@ -0,0 +1 @@ +../../../abi/Types.idr \ No newline at end of file diff --git a/src/idris-abi/Januskey/ABI/Foreign.idr b/src/idris-abi/Januskey/ABI/Foreign.idr new file mode 120000 index 0000000..7495952 --- /dev/null +++ b/src/idris-abi/Januskey/ABI/Foreign.idr @@ -0,0 +1 @@ +../../../abi/Foreign.idr \ No newline at end of file diff --git a/src/idris-abi/januskey-abi.ipkg b/src/idris-abi/januskey-abi.ipkg new file mode 100644 index 0000000..bdf9f92 --- /dev/null +++ b/src/idris-abi/januskey-abi.ipkg @@ -0,0 +1,30 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) Jonathan D.A. Jewell +-- +-- Idris2 package for the JanusKey ABI layer (src/abi/*.idr). +-- +-- Idris2 resolves module A.B.C to /A/B/C.idr, but the ABI sources +-- live flat in src/abi/ (Types.idr declares JanusKey.ABI.Types, etc.), so no +-- sourcedir value can reach them directly. They also cannot be moved: the +-- aspect tests, the Mustfile and the Zig FFI all name src/abi/.idr. +-- This directory therefore holds relative symlinks laid out by module name, +-- each pointing back to the single real file in src/abi/. +-- +-- Known defect, deliberately NOT fixed here (tracked as J1-3): +-- src/abi/Foreign.idr declares `Januskey.ABI.Foreign` (lowercase k) while +-- Proofs.idr imports `JanusKey.ABI.Foreign`; Foreign.idr in turn imports +-- `Januskey.ABI.Types` and `Januskey.ABI.Layout`, which no file declares. The +-- module is listed below under the name it actually declares, so these +-- imports fail to resolve until J1-3 normalises the casing. +-- The Januskey/ and JanusKey/ directories also collide on case-insensitive +-- filesystems (macOS/Windows default); typecheck on Linux. +-- +-- Run: idris2 --typecheck src/idris-abi/januskey-abi.ipkg (or: just test-proofs) +package januskey-abi + +sourcedir = "." + +modules = JanusKey.ABI.Types + , JanusKey.ABI.Layout + , Januskey.ABI.Foreign + , JanusKey.ABI.Proofs