ArghDA M4: Idris2 backend + --backend selector — genuinely multi-backend#34
Merged
Merged
Conversation
The second backend, on the M1 trait. arghda now drives two provers, chosen at the CLI with `--backend agda|idris2`. Idris2 is a core estate language (it owns ABIs — the Idris2-ABI / Zig-FFI pattern), so it's a first-class backend, not merely a prover. - `src/prover/idris2.rs` — `Idris2` impl: `idris2 --check --source-dir <root> <file>` (the `-i` analog, ground-truthed against Idris2 0.7.0), exit-code -only verdict (0→Proven, ran-nonzero→Error, absent→Unavailable). Dotted module names reuse `graph::module_name_of`; `.idr` `module_to_path`; an Idris2 import parser (`import [public] Mod [as Alias]`, top-level — no `open`); `Main.idr` root discovery. - `src/lint/idris2.rs` — `Idris2EscapeHatch` flags `believe_me`/ `assert_total`/`assert_smaller`/`idris_crash` + `%default partial`. Named `escape-hatch` on purpose so it reuses the reasoning-graph's amber cap — a `believe_me` is treated identically across backends. - `src/main.rs` — new `--backend agda|idris2` on scan/check/dag/reason via `backend_for()`; unknown backend errors cleanly. (Wire first — the backend is reachable, not just present.) - CLI `about` now reflects multi-backend (Agda, Idris2). - Tests: +9 unit (backend identity, `.idr` path mapping, import parser incl. public/alias, check_file honesty; escape-hatch rule) +3 integration (the graph/dag/reason path is hermetic — text parsing, no binary needed). Suite 93 green; clippy -D warnings, fmt, SPDX clean. - Dogfooded with REAL idris2 on PATH: `check --backend idris2` → proven-eligible; `reason --backend idris2 --check` → live typechecks, Main cone proven+wired, Orphan proven-but-unwired (the honest wired-vs-sound distinction). - STATE.a2ml records M4 = 90% (.ipkg roots + totality-hole lint are the documented follow-on 10%). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012MpYSh6Wy8YMBH2E3qVyT7
hyperpolymath
marked this pull request as ready for review
July 1, 2026 08:38
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What & why
The second backend, on the M1 trait — arghda now drives two provers, chosen at the CLI with
--backend agda|idris2. Idris2 is a core estate language (it owns ABIs — the Idris2-ABI / Zig-FFI pattern), so it's first-class, not merely a prover.Changes
src/prover/idris2.rs—Idris2impl:idris2 --check --source-dir <root> <file>(the-iinclude-root analog, ground-truthed against Idris2 0.7.0), exit-code-only verdict (0→Proven, ran-nonzero→Error, absent→Unavailable). Dotted module names reusegraph::module_name_of;.idrmodule_to_path; an Idris2 import parser (import [public] Mod [as Alias], top-level — noopen);Main.idrroot discovery.src/lint/idris2.rs—Idris2EscapeHatchflagsbelieve_me/assert_total/assert_smaller/idris_crash+%default partial. Deliberately namedescape-hatchso it reuses the reasoning-graph's amber cap — abelieve_meis treated identically across Agda and Idris2.src/main.rs— new--backend agda|idris2on scan/check/dag/reason viabackend_for(); unknown backend errors cleanly. (Wire first — the backend is reachable, not just present.) CLIaboutnow reflects multi-backend.Verified (ran, not inferred)
cargo test→ 93 passing, 0 failed (70 lib + 23 integration; +9 Idris2 unit: backend identity,.idrpath mapping, import parser incl. public/alias,check_filehonesty, escape-hatch rule; +3 Idris2 integration). The graph/dag/reason tests are hermetic — text parsing only, no binary needed, so CI is unaffected by whetheridris2is installed.cargo clippy -D warningsclean ·cargo fmt --checkclean ·check-spdx.shOK.arghda check --backend idris2 …/Main.idr→ real typecheck →proven-eligiblearghda reason --backend idris2 --check→ live typechecks each node → Main coneproven+wired,Orphanproven-but-wired=false(the honest wired-vs-sound distinction working)--backend lean4→Error: unknown backend lean4 (known: agda, idris2)Honest scope
M4 = ~90%. The documented follow-on 10%:
.ipkg-declared roots (currentlyMain.idrdiscovery) and totality-hole (?name) + per-defpartiallint.build/idris2 output is gitignored.Next
M5 SMT solvers (Z3/CVC5) — the first Solver-kind backend, exercising the other half of the taxonomy · M2 Cubical-Agda.
Generated by Claude Code