ArghDA M8: Coq/Rocq adapter — first heavy-tail backend (foundation-first)

[hyperpolymath]

What

The first of the heavy-tail backends. arghda is now a seven-backend prover-parametric workspace (agda, agda-cubical, idris2, lean4, coq as Assistants; z3, cvc5 as Solvers).

Done foundation-first: provisioned the toolchain before writing the adapter (opam 2.1.5 → coq.8.18.0), then built and dogfooded the backend against the real coqc.

How

Adapter — src/prover/rocq.rs (Coq)

• Assistant kind, extensions [v], command coqc.
• Verdict logic, ground-truthed vs Coq 8.18.0 — honest, never fabricated:
  • exit ≠ 0 → Error
  • exit 0 + Admitted/admit → Admitted
  • exit 0 + genuine postulate → Postulated
  • exit 0 clean → Proven (coqc kernel-checks every Qed at compile, so a clean compile with no escape hatch is honestly proven — stronger than Lean, which needs a #print axioms audit)
• count_genuine_postulates — the Section-aware classifier ported from panic-attack's count_rocq_unverified_postulates: Section-scoped Variable/Hypothesis/Parameter discharge at End; module-level Parameter of carrier / decidability-witness / non-Prop-function type are abstractions; Prop-valued Axiom/Parameter are counted.
• check_file redirects the .vo into a temp dir keeping the source stem (coqc -o requires target basename == source; a real-coqc dogfood caught the first attempt renaming it).
• Imports: Require [Import|Export] + From P Require …; bare Import/Export is a namespace directive, not an edge (as Lean open is). Roots: the All.v aggregator convention.

Lint — src/lint/coq.rs (CoqEscapeHatch): warn under the shared escape-hatch name (caps at amber in the reasoning graph); flags Admitted/admit/Axiom/Conjecture. Parameter is left to the backend's Section-aware classifier.

Wired: backend_for "coq", KNOWN_BACKENDS, all four --backend help strings, the CLI about line.

Verification (actually run)

• cargo fmt --check — clean
• cargo clippy --all-targets -- -D warnings — clean
• cargo test — 146 pass (+7 rocq unit, +5 coq lint unit, +3 coq integration; the graph tests are hermetic — text only, run tool-less)
• bash scripts/check-spdx.sh . — OK

Dogfooded against real coqc 8.18.0:

fixture	arghda check --backend coq
Clean.v (Qed)	proven
Admits.v (Admitted)	admitted
Postulate.v (Prop Axiom)	postulated
Broken.v (type error)	error

• reason --check --backend coq reproduces those verdicts
• import edge All → Base parsed; All.v discovered as crt_root; Base+Util wired; Orphan unwired
• arghda doctor → [OK] coq assistant The Coq Proof Assistant, version 8.18.0

Scope

M8 at 90%. Remaining: _CoqProject-driven logical-path resolution + dependency-ordered compilation (a bare single-file coqc reports Error when an uncompiled dependency is Required — a documented limitation, the same class as Lean's lake-env gap).

🤖 Generated with Claude Code

https://claude.ai/code/session_012MpYSh6Wy8YMBH2E3qVyT7

---

Generated by Claude Code