fix(idris2): make the dyadic parse front-end actually compile + gate it in CI (#340)

## What

A ground-truth verification sweep ("everything claimed done must be
checked with the actual provers/toolchains") found the `idris2/` dyadic
parse front-end had **never been compiled**:

- all 14 `idris2/src/**.idr` files carried a `// Owner:` header — Zig/C
comment syntax, an Idris2 **syntax error** (owner-header hook used the
wrong comment leader);
- `Tests.idr` had five further never-elaborated defects underneath: an
escaped `\\t =>` lambda, a `Nat`/`Int` mismatch at `newBuf`, a missing
`import Ephapax.Parse.Util` (source of `ParseError`),
definition-before-use ordering (`parseWithBuf`/tests after `runTests`),
un-exported `runTests` (which `TestMain` imports), `mapM_` (not Idris2
Prelude), and `%default total` over a `covering` parser;
- **no CI workflow builds `idris2/*.ipkg` or `src/formal/*.ipkg`**, so
nothing ever caught any of this.

## Changes

- Fix headers to `--` in all 14 files; repair
`Tests.idr`/`TestMain.idr`.
- `abi-verify.yml`: add `idris2-formal` + `idris2-parse-front` build
gates (compile-time; the runtime FFI path is covered by
`ffi-seams.yml`'s zig tests + documented local run).
- Bump idris2 pin 0.7.0 → 0.8.0 (`.tool-versions`,
`scripts/install-idris2.sh`) — 0.8.0 is what everything verifiably
builds with.
- `TEST-NEEDS.md`: record the parse-tests suite as compile+run verified,
and `ephapax-affine.ipkg` as still un-gated (external `proven`
dependency).

## Verification (all local, 2026-07-07)

| Oracle | Result |
|---|---|
| `idris2 --build ephapax-abi.ipkg` (0.8.0) | 3/3 modules ✅ |
| `idris2 --build ephapax-formal.ipkg` | 3/3 modules ✅ |
| `idris2 --build ephapax-parse-tests.ipkg` | 8/8 modules + executable ✅
|
| Run `ephapax-parse-tests` against zig-built `libephapax_tokbuf.so`
(`-lc`) | `parse-tests: ok`, exit 0 ✅ |
| `zig test` tokbuf seams + coproc | 12/12 ✅ |
| Fresh `coqc` 8.18.0 rebuild of `formal/` | exit 0; `Print Assumptions`
closed except the documented `preservation_l1` Admitted ✅ |
| `cargo test --workspace` | exit 0 ✅ |
| `just validate-wasm` (wasm-tools 1.252.0) | all modules structurally
valid ✅ |

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

Author: hyperpolymath

.github/workflows/abi-verify.yml

@@ -21,11 +21,15 @@ on:
   pull_request:
     paths:
       - 'src/abi/**'
+      - 'src/formal/**'
+      - 'idris2/**'
       - '.github/workflows/abi-verify.yml'
   push:
     branches: [main]
     paths:
       - 'src/abi/**'
+      - 'src/formal/**'
+      - 'idris2/**'
 
 permissions:
   contents: read
@@ -56,3 +60,45 @@ jobs:
           # well-typed and do NOT fail the build — they are tracked in
           # PROOF-NEEDS.md, not hidden.
           idris2 --build ephapax-abi.ipkg
+
+  idris2-formal:
+    name: Idris2 formal seam (ephapax-formal.ipkg)
+    runs-on: ubuntu-latest
+    timeout-minutes: 20
+    container:
+      image: snazzybucket/idris2:latest  # estate-standard Idris2 image
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0  # v4
+
+      - name: Build (typecheck) the formal package
+        working-directory: src/formal
+        run: |
+          idris2 --version
+          idris2 --build ephapax-formal.ipkg
+
+  idris2-parse-front:
+    name: Idris2 parse front-end (ephapax-parse-tests.ipkg)
+    runs-on: ubuntu-latest
+    timeout-minutes: 20
+    container:
+      image: snazzybucket/idris2:latest  # estate-standard Idris2 image
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0  # v4
+
+      - name: Build the parse front-end + test executable
+        working-directory: idris2
+        run: |
+          idris2 --version
+          # Compile-time gate only: the %foreign C bindings in
+          # Parse/ZigBuffer.idr resolve libephapax_tokbuf at RUNTIME
+          # (Chez dlopen), so building the executable needs no zig.
+          # Running it does — that path is exercised locally via
+          #   zig build-lib -dynamic -lc ffi/zig/tokbuf.zig \
+          #     -femit-bin=libephapax_tokbuf.so
+          #   LD_LIBRARY_PATH=. ./build/exec/ephapax-parse-tests
+          # and the zig side is unit-gated by ffi-seams.yml.
+          # (ephapax-affine.ipkg is NOT gated here: it depends on the
+          # external `proven` package — see PROOF-NEEDS.md.)
+          idris2 --build ephapax-parse-tests.ipkg

.tool-versions

@@ -8,5 +8,5 @@ ocaml 5.4.1
 # directly; coq is provisioned via apt (noble ships exactly 8.18.0), kept
 # here only as the documented pin.
 coq 8.18.0
-idris2 0.7.0
+idris2 0.8.0
 zig 0.14.0

TEST-NEEDS.md

@@ -66,6 +66,13 @@ reads from there.
 ### Build & Execution
 - [x] cargo build — compiles
 - [x] cargo test --workspace --all-targets — 467 pass, 0 fail
+- [x] idris2/ephapax-parse-tests.ipkg — compiles AND runs green (2026-07-07,
+  idris2 0.8.0 + zig-built libephapax_tokbuf.so); CI-gated compile-only by
+  abi-verify.yml `idris2-parse-front` (runtime run stays local — the estate
+  idris2 container has no zig)
+- [ ] idris2/ephapax-affine.ipkg — NOT CI-gated: depends on the external
+  `proven` Idris2 package (hyperpolymath/proven), which the estate idris2
+  image does not carry. Gate once proven is installable in CI (or vendored).
 - [ ] Compile and run all 98 .eph files — not automated
 - [ ] CLI --help works — not verified
 - [ ] Self-diagnostic — none

idris2/src/Ephapax/Affine/Emit.idr

@@ -1,5 +1,5 @@
 -- SPDX-License-Identifier: MPL-2.0
-// Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+-- Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 -- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 --
 module Ephapax.Affine.Emit

idris2/src/Ephapax/Affine/Typecheck.idr

@@ -1,5 +1,5 @@
 -- SPDX-License-Identifier: MPL-2.0
-// Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+-- Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 -- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 --
 module Ephapax.Affine.Typecheck

idris2/src/Ephapax/IR/AST.idr

@@ -1,5 +1,5 @@
 -- SPDX-License-Identifier: MPL-2.0
-// Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+-- Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 -- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 --
 module Ephapax.IR.AST

idris2/src/Ephapax/IR/Decode.idr

@@ -1,5 +1,5 @@
 -- SPDX-License-Identifier: MPL-2.0
-// Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+-- Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 -- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 --
 module Ephapax.IR.Decode

idris2/src/Ephapax/IR/SExpr.idr

@@ -1,5 +1,5 @@
 -- SPDX-License-Identifier: MPL-2.0
-// Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+-- Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 -- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 --
 module Ephapax.IR.SExpr

idris2/src/Ephapax/Parse/Lexer.idr

@@ -1,5 +1,5 @@
 -- SPDX-License-Identifier: MPL-2.0
-// Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+-- Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 -- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 --
 module Ephapax.Parse.Lexer

idris2/src/Ephapax/Parse/Parser.idr

@@ -1,5 +1,5 @@
 -- SPDX-License-Identifier: MPL-2.0
-// Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+-- Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 -- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 --
 module Ephapax.Parse.Parser