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

.machine_readable/6a2/STATE.a2ml

@@ -11,7 +11,7 @@ status = "active"  # active | paused | archived
 
 [project-context]
 name = "arghda-core"
-purpose = "Multi-backend proof-workspace manager — the 'Flying Logic for provers/solvers' engine. A four-state triage workspace (inbox/working/proven/rejected) as file moves, per-backend lint packs targeting the silent-failure class, a backend-parametric import-graph DAG, a demote-only status-propagating reasoning graph, and a JSON + event-stream contract a visual layer (arghda-studio) consumes. Six backends across both interaction models (Agda, Cubical-Agda, Idris2, Lean4 assistants; Z3, CVC5 solvers). It never proves anything itself; the tools do."
+purpose = "Multi-backend proof-workspace manager — the 'Flying Logic for provers/solvers' engine. A four-state triage workspace (inbox/working/proven/rejected) as file moves, per-backend lint packs targeting the silent-failure class, a backend-parametric import-graph DAG, a demote-only status-propagating reasoning graph, and a JSON + event-stream contract a visual layer (arghda-studio) consumes. Seven backends across both interaction models (Agda, Cubical-Agda, Idris2, Lean4, Coq/Rocq assistants; Z3, CVC5 solvers). It never proves anything itself; the tools do."
 completion-percentage = 92
 
 [position]
@@ -48,15 +48,18 @@ milestones = [
   { name = "M5: SMT solver backends (Z3, CVC5): SMT-LIB2 -> sat/unsat/unknown -> Verdict", completion = 100 },
   { name = "M6: Lean4 adapter (lake build + #print axioms audit)", completion = 92 },
   { name = "M7: Echidna dispatch seam (optional route to orchestrator :8090, same Outcome)", completion = 70 },
-  { name = "M8: Coq/Rocq adapter (--heavy provisioning; Section-aware postulate classifier)", completion = 0 },
+  { name = "M8: Coq/Rocq adapter (--heavy provisioning; Section-aware postulate classifier)", completion = 90 },
   { name = "M9: Isabelle adapter (--heavy; dogfood tropical-resource-typing .thy)", completion = 0 },
   { name = "M10: Mizar adapter (detect-only first; highest uncertainty)", completion = 0 },
   { name = "M11: studio JSON freeze (reason/0.1) + Groove manifest", completion = 100 },
 ]
 # M0 provisioning verified in-container 2026-07-01: agda 2.6.3 (+stdlib v2.3
 # +cubical lib), zig 0.15.2, z3 4.8.12, cvc5 1.2.0, lean 4.13.0 all report
-# real --version. idris2 v0.7.0 builds via chez bootstrap. Coq/Isabelle/Mizar
-# are scripted (behind --heavy/--mizar) but not installed this session.
+# real --version. idris2 v0.7.0 builds via chez bootstrap. COQ NOW INSTALLED
+# (2026-07-01, heavy-tail foundation): opam 2.1.5 via apt → `opam install
+# coq.8.18.0` → coqc reports real --version; symlinked to /usr/local/bin/coqc
+# so `arghda doctor` probes it ([OK] coq assistant). Isabelle/Mizar remain
+# scripted (behind --heavy/--mizar) but not installed this session.
 # Remaining M0: `arghda doctor` Rust subcommand (interim: `just doctor` shells
 # the script's --verify-only table).
 #
@@ -116,6 +119,36 @@ milestones = [
 # proven root → unknown; edit the proven file on disk → Good demoted to unknown
 # with the stale evidence string. M3 base was 100%; this is pure additive refinement.
 #
+# M8 landed 2026-07-01 (90%, first heavy-tail backend): the Coq/Rocq adapter.
+# Foundation-first — provisioned coqc 8.18.0 (opam) BEFORE the adapter, then
+# built + dogfooded against the REAL tool. src/prover/rocq.rs (`Coq`): Assistant
+# kind, extensions [v], command `coqc`. Verdict logic, ground-truthed vs Coq
+# 8.18.0: 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 this is honest — stronger than Lean's need for a
+# #print axioms audit). "Genuine postulate" = `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/
+# non-Prop-function type are abstractions; Prop-valued Axiom/Parameter counted.
+# check_file redirects the .vo to a temp DIR keeping the source stem (coqc `-o`
+# insists target basename == source; a REAL-coqc dogfood caught my first
+# attempt renaming it). Imports: `Require [Import|Export]` + `From P Require …`
+# (bare Import/Export = namespace directive, not an edge, like Lean `open`).
+# Roots: `All.v` aggregator convention (mirrors Agda). Lint: src/lint/coq.rs
+# `CoqEscapeHatch` (warn, shared name `escape-hatch`) flags Admitted/admit/
+# Axiom/Conjecture (Parameter left to the backend classifier). Wired: backend_for
+# "coq" + KNOWN_BACKENDS + all four `--backend` help strings + about line.
+# 146 tests (+7 rocq unit +5 coq lint unit +3 coq integration; graph tests
+# hermetic — text only, run tool-less). DOGFOODED vs real coqc 8.18.0: check
+# → Clean=proven / Admits=admitted / Postulate=postulated / Broken=error;
+# `reason --check --backend coq` reproduces those; import edge All→Base parsed,
+# All.v discovered as crt_root, Base+Util wired, Orphan unwired; `doctor` →
+# [OK] coq assistant 8.18.0. Remaining 10%: `_CoqProject`-driven logical-path
+# resolution + dependency-ordered compilation (a bare single-file coqc reports
+# Error when an uncompiled dependency is Required — documented limitation, same
+# class as Lean's lake-env gap).
+#
 # M7 landed 2026-07-01 (70%): the Echidna dispatch seam — completes the
 # engine-spine deliverable (M0-M7 + M11). src/dispatch.rs: `Dispatch { Local,
 # Echidna { base_url } }` + `run(backend, file, include_root) -> Outcome`
@@ -277,7 +310,8 @@ actions = [
   "M6 follow-on: #print axioms audit DONE (import-free files promote honestly); remaining = lake-env/LEAN_PATH so imported files can be checked + audited too.",
   "M4 follow-on: .ipkg-declared roots DONE; remaining = totality-hole (?name) + per-def `partial` lint.",
   "M3 follow-on: DONE — `reason --workspace <ws>` sources real verdicts from a `proven/` state (workspace_verdicts) + demotes stale-proven via the content-hash closure. Refinement follow-ons bucket now complete.",
-  "M8-M10 heavy tail (Coq/Rocq, Isabelle, Mizar) — gated on --heavy provisioning (Coq via opam ~1hr; Isabelle ~4GB; Mizar niche).",
+  "M8 (Coq/Rocq): DONE (90%) — coqc 8.18.0 provisioned + adapter built + dogfooded (proven/admitted/postulated/error) with Section-aware postulate classifier. Remaining: _CoqProject logical paths + dependency-ordered compilation.",
+  "M9-M10 heavy tail (Isabelle, Mizar) — next, foundation-first: Isabelle ~4GB tarball then adapter; Mizar niche/detect-only. Then climb to M6 lake-env, M4 totality lint, M7 Echidna client.",
 ]
 
 [maintenance-status]
@@ -286,13 +320,13 @@ last-result = "pass"  # unknown | pass | warn | fail
 open-warnings = 0
 open-failures = 0
 # `just check` (fmt-check + clippy -D warnings + build + test + SPDX) green
-# post-M3-followon: 96 lib + 34 integration = 130 tests pass. codeql.yml added
-# (code-scanning gate fix). reason --workspace verdicts+staleness dogfooded.
-# Lean #print axioms audit dogfooded. doctor/groove/dispatch
-# dogfooded: 6/6 backends runnable; groove writes /.well-known/groove; --dispatch
-# local real, echidna honest-stub. All six backends dogfooded via real CLI: agda
-# + agda-cubical + idris2 + lean4 (Assistant), z3 + cvc5 (Solver). Dogfooded
-# historically vs echo-types + agda-unused.
+# post-M8: 108 lib + 38 integration = 146 tests pass. codeql.yml added
+# (code-scanning gate fix). M8 Coq adapter dogfooded vs real coqc 8.18.0
+# (proven/admitted/postulated/error; reason --check; import edges; roots; wired;
+# doctor [OK] coq). reason --workspace verdicts+staleness dogfooded. Lean
+# #print axioms audit dogfooded. doctor/groove/dispatch dogfooded. SEVEN
+# backends now: agda + agda-cubical + idris2 + lean4 + coq (Assistant), z3 +
+# cvc5 (Solver). Dogfooded historically vs echo-types + agda-unused.
 
 [ecosystem]
 part-of = ["arghda"]

src/lib.rs

@@ -35,8 +35,8 @@ pub use graph::{build as build_graph, ImportGraph};
 pub use groove::{manifest as groove_manifest, GrooveManifest};
 pub use lint::{default_rules, rules_with_config, run_lints, LintRule, RuleConfig};
 pub use prover::{
-    default_backend, Agda, AgdaCubical, Backend, BackendKind, Idris2, Lean, Outcome, Probe, Smt,
-    Verdict,
+    default_backend, Agda, AgdaCubical, Backend, BackendKind, Coq, Idris2, Lean, Outcome, Probe,
+    Smt, Verdict,
 };
 pub use reason::{
     build as build_reason, workspace_verdicts, Junct, ReasonDocument, ReasonEdge, ReasonNode,

src/lint/coq.rs

@@ -0,0 +1,154 @@
+// SPDX-License-Identifier: MPL-2.0
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+
+//! Coq / Rocq `escape-hatch` (warn) — surface soundness escape hatches.
+//!
+//! The Coq analogue of the Agda/Idris2/Lean escape-hatch rules; shares the
+//! rule *name* `escape-hatch` so the reasoning graph caps any hit at amber.
+//!
+//! Flags the unambiguous holes: `Admitted`/`admit` (a proof closed as an
+//! axiom / left as a placeholder) and `Axiom`/`Conjecture` (declared, not
+//! proved). `coqc` compiles all of these with exit 0, so without this warn —
+//! and without the backend's Section-aware postulate classification — they
+//! ride along invisibly. `Parameter`/`Variable`/`Hypothesis` are deliberately
+//! NOT flagged here: they are legitimate scaffold shapes far more often than
+//! not, and the genuine module-level `Parameter` postulate is caught by the
+//! backend's `count_genuine_postulates` (Section-aware) instead.
+
+use super::{LintContext, LintRule};
+use crate::diagnostic::{Diagnostic, LintReport, Severity};
+use anyhow::{Context, Result};
+use std::fs;
+use std::path::Path;
+
+pub struct CoqEscapeHatch;
+
+const ESCAPE_TOKENS: &[&str] = &["Admitted", "admit", "Axiom", "Conjecture"];
+
+impl LintRule for CoqEscapeHatch {
+    fn name(&self) -> &'static str {
+        "escape-hatch"
+    }
+
+    fn run(&self, file: &Path, _ctx: &LintContext<'_>, report: &mut LintReport) -> Result<()> {
+        let contents =
+            fs::read_to_string(file).with_context(|| format!("reading {}", file.display()))?;
+        for (i, raw) in contents.lines().enumerate() {
+            let trimmed = raw.trim_start();
+            if trimmed.starts_with("(*") {
+                continue; // whole-line comment (common case)
+            }
+            let code = strip_line_comments(raw);
+            for tok in ESCAPE_TOKENS {
+                if has_token(&code, tok) {
+                    report.push(warn(
+                        self.name(),
+                        file,
+                        i + 1,
+                        format!("escape primitive `{tok}`"),
+                    ));
+                }
+            }
+        }
+        Ok(())
+    }
+}
+
+fn warn(rule: &str, file: &Path, line: usize, message: String) -> Diagnostic {
+    Diagnostic {
+        rule: rule.to_string(),
+        severity: Severity::Warn,
+        file: file.to_path_buf(),
+        message,
+        line: Some(line),
+    }
+}
+
+/// Remove balanced `(* … *)` spans; an unmatched `(*` truncates the rest of
+/// the line.
+fn strip_line_comments(line: &str) -> String {
+    let mut out = String::with_capacity(line.len());
+    let bytes = line.as_bytes();
+    let mut i = 0;
+    let mut depth = 0u32;
+    while i < bytes.len() {
+        if i + 1 < bytes.len() && bytes[i] == b'(' && bytes[i + 1] == b'*' {
+            depth += 1;
+            i += 2;
+            continue;
+        }
+        if depth > 0 && i + 1 < bytes.len() && bytes[i] == b'*' && bytes[i + 1] == b')' {
+            depth -= 1;
+            i += 2;
+            continue;
+        }
+        if depth == 0 {
+            out.push(bytes[i] as char);
+        }
+        i += 1;
+    }
+    out
+}
+
+/// `tok` appears in `s` as a delimited token (so `admittedly` or `Foo.admit`
+/// do not match the bare keyword).
+fn has_token(s: &str, tok: &str) -> bool {
+    s.split(|c: char| c.is_whitespace() || "(){};,.".contains(c))
+        .any(|w| w == tok)
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use crate::lint::run_lints;
+    use std::path::PathBuf;
+
+    fn lint_str(body: &str) -> LintReport {
+        let tmp = tempfile::NamedTempFile::new().unwrap();
+        std::fs::write(tmp.path(), body).unwrap();
+        let roots: [PathBuf; 0] = [];
+        let ctx = LintContext {
+            include_root: tmp.path().parent().unwrap(),
+            entry_modules: &roots,
+        };
+        let rules: Vec<Box<dyn LintRule>> = vec![Box::new(CoqEscapeHatch)];
+        run_lints(tmp.path(), &ctx, &rules).unwrap()
+    }
+
+    #[test]
+    fn admitted_is_warned() {
+        let r = lint_str("Theorem t : True.\nProof.\nAdmitted.\n");
+        assert_eq!(r.warns().count(), 1);
+        assert_eq!(r.diagnostics[0].rule, "escape-hatch");
+        assert!(r.diagnostics[0].message.contains("Admitted"));
+    }
+
+    #[test]
+    fn axiom_and_admit_tactic_are_warned() {
+        let r = lint_str(
+            "Axiom em : forall P : Prop, P \\/ ~P.\nTheorem t : True. Proof. admit. Defined.\n",
+        );
+        assert_eq!(r.warns().count(), 2);
+    }
+
+    #[test]
+    fn escape_token_in_comment_is_ignored() {
+        let r = lint_str("Definition x := 0. (* no Admitted here *)\n");
+        assert!(r.diagnostics.is_empty());
+        let r2 = lint_str("(* Axiom foo : bar. *)\n");
+        assert!(r2.diagnostics.is_empty());
+    }
+
+    #[test]
+    fn clean_coq_file_is_silent() {
+        let r = lint_str("Theorem t : True.\nProof.\nexact I.\nQed.\n");
+        assert!(r.diagnostics.is_empty());
+    }
+
+    #[test]
+    fn parameter_is_not_flagged_by_the_lint() {
+        // Parameter is left to the backend's Section-aware classifier.
+        let r = lint_str("Parameter State : Type.\n");
+        assert!(r.diagnostics.is_empty());
+    }
+}

src/lint/mod.rs

@@ -5,6 +5,7 @@ use crate::diagnostic::LintReport;
 use anyhow::Result;
 use std::path::{Path, PathBuf};
 
+pub mod coq;
 pub mod escape_hatch;
 pub mod idris2;
 pub mod lean;

src/main.rs

@@ -5,8 +5,8 @@ use anyhow::{Context, Result};
 use arghda_core::lint::LintContext;
 use arghda_core::{
     build_dag, build_reason, event, groove_manifest, run_lints, unused, watcher, Agda, AgdaCubical,
-    Backend, BackendKind, Dispatch, Idris2, Lean, LintRule, Probe, RuleConfig, Smt, State, Verdict,
-    Workspace,
+    Backend, BackendKind, Coq, Dispatch, Idris2, Lean, LintRule, Probe, RuleConfig, Smt, State,
+    Verdict, Workspace,
 };
 use clap::{Parser, Subcommand};
 use std::path::{Path, PathBuf};
@@ -17,7 +17,15 @@ use walkdir::WalkDir;
 type RuleSet = Vec<Box<dyn LintRule>>;
 
 /// Every backend `--backend` accepts and `doctor` probes.
-const KNOWN_BACKENDS: &[&str] = &["agda", "agda-cubical", "idris2", "lean4", "z3", "cvc5"];
+const KNOWN_BACKENDS: &[&str] = &[
+    "agda",
+    "agda-cubical",
+    "idris2",
+    "lean4",
+    "coq",
+    "z3",
+    "cvc5",
+];
 
 /// Resolve a `--backend` name to a backend instance. Agda is the default and
 /// v0.1 reference; Idris2 is the estate ABI language.
@@ -27,10 +35,11 @@ fn backend_for(name: &str) -> Result<Box<dyn Backend>> {
         "agda-cubical" => Ok(Box::new(AgdaCubical)),
         "idris2" => Ok(Box::new(Idris2)),
         "lean4" => Ok(Box::new(Lean)),
+        "coq" => Ok(Box::new(Coq)),
         "z3" => Ok(Box::new(Smt::z3())),
         "cvc5" => Ok(Box::new(Smt::cvc5())),
         other => anyhow::bail!(
-            "unknown backend `{other}` (known: agda, agda-cubical, idris2, lean4, z3, cvc5)"
+            "unknown backend `{other}` (known: agda, agda-cubical, idris2, lean4, coq, z3, cvc5)"
         ),
     }
 }
@@ -39,7 +48,7 @@ fn backend_for(name: &str) -> Result<Box<dyn Backend>> {
 #[command(
     name = "arghda",
     version,
-    about = "Proof-workspace manager for provers/solvers (Agda, Cubical, Idris2, Lean4, Z3, CVC5)"
+    about = "Proof-workspace manager for provers/solvers (Agda, Cubical, Idris2, Lean4, Coq, Z3, CVC5)"
 )]
 struct Cli {
     #[command(subcommand)]
@@ -67,7 +76,7 @@ enum Cmd {
         #[arg(long)]
         config: Option<PathBuf>,
         /// Backend: `agda` (default), `agda-cubical`, `idris2`, `lean4`,
-        /// `z3`, `cvc5`.
+        /// `coq`, `z3`, `cvc5`.
         #[arg(long, default_value = "agda")]
         backend: String,
         /// Also run the external `agda-unused` analyser and re-emit its
@@ -87,7 +96,7 @@ enum Cmd {
         #[arg(long)]
         include_root: Option<PathBuf>,
         /// Backend: `agda` (default), `agda-cubical`, `idris2`, `lean4`,
-        /// `z3`, `cvc5`.
+        /// `coq`, `z3`, `cvc5`.
         #[arg(long, default_value = "agda")]
         backend: String,
         /// Where the check runs: `local` (default) or `echidna[=<url>]`
@@ -115,7 +124,7 @@ enum Cmd {
         #[arg(long)]
         config: Option<PathBuf>,
         /// Backend: `agda` (default), `agda-cubical`, `idris2`, `lean4`,
-        /// `z3`, `cvc5`.
+        /// `coq`, `z3`, `cvc5`.
         #[arg(long, default_value = "agda")]
         backend: String,
     },
@@ -139,7 +148,7 @@ enum Cmd {
         #[arg(long)]
         config: Option<PathBuf>,
         /// Backend: `agda` (default), `agda-cubical`, `idris2`, `lean4`,
-        /// `z3`, `cvc5`.
+        /// `coq`, `z3`, `cvc5`.
         #[arg(long, default_value = "agda")]
         backend: String,
         /// Run the backend on every node to populate REAL prover verdicts

src/prover/mod.rs

@@ -30,11 +30,13 @@ use std::process::Command;
 pub mod agda;
 pub mod idris2;
 pub mod lean;
+pub mod rocq;
 pub mod smt;
 
 pub use agda::{Agda, AgdaCubical};
 pub use idris2::Idris2;
 pub use lean::Lean;
+pub use rocq::Coq;
 pub use smt::Smt;
 
 /// The two backend interaction models.