ArghDA → Flying Logic for provers/solvers: M0 (toolchain provisioning + doctor)#31
Merged
Merged
Conversation
check-spdx.sh set the prose SPDX variable to MPL-2.0, which contradicted the repo's own machine-readable declaration (licensing-policy.toml: prose = CC-BY-SA-4.0) and the checker's own failure label. Every prose file already carries CC-BY-SA-4.0, so the checker was failing `just license-check` on a pristine tree. Point the variable at the declared policy and exclude the canonical LICENSES/ REUSE texts (mirrored in licensing-policy.toml). No licence header on any file is changed — this only corrects the enforcer to accept the headers that are already present and declared. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012MpYSh6Wy8YMBH2E3qVyT7
…doctor Adds scripts/provision-provers.sh: an idempotent, version-pinned installer for the prover/solver backends ArghDA drives, modelled on echo-types' provision-agda.sh and widened to the full set. Tractable tier (installed by default): agda 2.6.3 + stdlib v2.3 + the agda/cubical library, zig 0.15.2, idris2 v0.7.0 (chez bootstrap), lean4 v4.13.0 (elan), and the SMT solvers z3 + cvc5 1.2.0. Heavy tier behind --heavy (coq via opam, isabelle) and --mizar. Honesty contract: a backend is only ever reported OK when its own --version returned 0 in the run; anything else is MISSING/FAILED with the command tried. Third-party sources are fetched as curl tarballs rather than `git clone`, because this environment's proxy 403s git-relay access to non-scoped repos (and tarballs are more portable anyway). Justfile gains `provision` / `provision-heavy` / `doctor` recipes (the interim doctor shells the script's --verify-only table until the `arghda doctor` subcommand lands). STATE.a2ml records M0 and the Flying-Logic multi-prover epic (M1–M11). 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 02:57
hyperpolymath
added a commit
that referenced
this pull request
Jul 1, 2026
## What & why The keystone of the "Flying Logic for provers/solvers" epic. Every Agda-baked seam now lives behind an object-safe `Backend` trait, so the four-state workspace, DAG builder, content-hash invalidation and the cycle-safe reachability walk become backend-neutral. Agda is the first (v0.1 reference) impl; adding Idris2 / Lean4 / Z3 / CVC5 / Coq / Isabelle / Mizar is now *an impl*, not a rewrite. Follow-on from M0 (toolchain provisioning, merged as #31). #31 being merged, this is a fresh PR on the same working branch. ## This is a pure refactor — the test suite is the oracle Behaviour is unchanged, ground-truthed by running the tools (not inferred): - **`cargo test`** — the 64 pre-existing tests (50 lib + 14 integration) all stay green; +2 new Agda-backend tests = **66 passing, 0 failed**. - **`cargo clippy --all-targets --all-features -- -D warnings`** — clean. - **`cargo fmt --check`** — clean. - **`scripts/check-spdx.sh .`** — `SPDX licence invariant: OK`. - **Dogfood** — `arghda dag tests/fixtures/wellformed` emits byte-compatible JSON (`version: "0.1"`, same nodes/edges); `arghda check …/All.agda` ran a **real** Agda typecheck → `proven-eligible` (agda is present from #31's provisioning). ## Changes **New `src/prover/`:** - `Backend` trait — `name` / `kind` / `extensions` / `safe_mode` / `check_file` + the import-graph trio (`module_name_of` / `module_to_path` / `direct_imports`) + `discover_roots` + `lint_rules`. - `BackendKind { Assistant, Solver }` — the two interaction models (typecheck-a-file vs SMT query). - `Verdict { Proven, Refuted, Unknown, Admitted, Postulated, Error, Unavailable }` — the common verdict both models map into. **Only `Proven` is green; `Admitted`/`Postulated` are amber.** - `Outcome` — superset of the old `AgdaOutcome` (raw process facts + `kind` + `verdict`). **Refactor:** - `src/agda.rs` → `src/prover/agda.rs`. `Agda` is the first impl: owns the `agda` shell-out, delegates parsing to `graph::` free fns and the lint pack to `lint::`. Verdict is **exit-code-only** (0 → `Proven`, ran-nonzero → `Error`, absent → `Unavailable`) — arghda never claims a result Agda did not return; `Admitted`/`Postulated` stay lint-derived, never manufactured from a green exit. - `graph::build` and `dag::build` take `&dyn Backend` and use the backend's extension filter + import parsing. **The cycle-safe reachability walk and its `transitive_imports_terminates_on_a_cycle` regression are untouched** — cycle safety is inherited free by every backend. - `main.rs` `scan`/`check`/`dag`/`resolve_roots_and_rules` route through the backend; the `check` JSON key `agda` → `backend` (now carries `kind` + `verdict`). - `STATE.a2ml` records M1 = 100%; `.gitignore` ignores `*.agdai`. ## Honesty note (owner directive + AGENTIC.a2ml) The `Backend` module is the boundary where "never report a verdict the tool did not emit" is enforced: `check_file` derives its verdict from the actual exit code and degrades to `Unavailable` when the binary is absent. ## Next (trait now stable → parallelisable) M3 reasoning-graph (`src/reason`), M4 Idris2, M5 SMT (Z3/CVC5), M2 Cubical-Agda. --- _Generated by [Claude Code](https://claude.ai/code/session_012MpYSh6Wy8YMBH2E3qVyT7)_ Co-authored-by: Claude <noreply@anthropic.com>
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.
Context
First increment of the epic to evolve
arghda-corefrom an Agda-only proof-workspace engine into a "Flying Logic for provers/solvers" — a multi-backend, status-propagating reasoning-graph workspace (Agda-first, then Idris2, Lean4, Coq/Rocq, Isabelle, Cubical-Agda, Mizar, plus SMT solvers Z3/CVC5). The full plan phases the work M0→M11; this PR is M0: reproducible, honest toolchain provisioning — the fix for the recurring "guess a URL / get one wrong / nothing installs" pain.Guiding invariant throughout the epic: never embed a prover, and never report a verdict a real run didn't produce.
What's in this PR
scripts/provision-provers.sh— idempotent, version-pinned installer for all backends. Tractable tier installed by default; heavy tier (Coq via opam, Isabelle) behind--heavy; Mizar behind--mizar. Honesty contract baked in: a backend is reportedOKonly when its own--versionreturned 0 in the run; everything else prints asMISSING/FAILEDwith the command tried. Third-party sources are fetched as curl tarballs, notgit clone— the environment's proxy 403s git-relay access to non-scoped repos, and tarballs are more portable anyway.Justfile—provision/provision-heavy/doctorrecipes (interimdoctorshells the script's--verify-onlytable until thearghda doctorRust subcommand lands).scripts/check-spdx.sh+licensing-policy.toml—MPL-2.0, contradicting the repo's own declared policy (prose = CC-BY-SA-4.0, which every prose file already carries) and the checker's own failure label. This was failingjust license-checkon a pristine tree. No licence header on any file was changed — only the enforcer, so it now accepts the already-present, already-declared headers; the canonicalLICENSES/texts are excluded. One-line revert if you'd prefer to handle it differently.STATE.a2ml— records M0 and the M1–M11 milestone ladder.Verified in-container (real
--versionoutput)--cubicalflag)--heavy/--mizar; not installed this sessionjust checkpasses (fmt + clippy-D warnings+ SPDX + build + 64 tests, 0 failed).Next (not in this PR)
M1 — the keystone: introduce a
Backendtrait spanning two kinds (proof-assistantAssistanttypecheck→exit-code;SolverSMT-LIB2→sat/unsat/unknown) with a commonVerdictenum, moveagda.rsbehind it as a pure refactor (the 64 tests are the oracle), then M3's Flying-Logic reasoning graph (And/Or juncts + demote-only status propagation).🤖 Generated with Claude Code
Generated by Claude Code