ArghDA M0 complete: arghda doctor — honest backend availability probe

.machine_readable/6a2/STATE.a2ml

@@ -40,7 +40,7 @@ milestones = [
 # "proven" on a real exit-0 (never embed a prover). See the plan doc.
 [route-to-flying-logic]
 milestones = [
-  { name = "M0: provision-provers.sh (pinned, honest --version verification) + `just provision/doctor` recipes", completion = 80 },
+  { name = "M0: provision-provers.sh (pinned, honest --version verification) + `just provision/doctor` recipes + `arghda doctor`", completion = 100 },
   { name = "M1: Backend trait (Assistant|Solver kinds; Outcome/Verdict); agda.rs -> prover/agda.rs; graph/dag take &dyn Backend (pure refactor, 50 tests stay green)", completion = 100 },
   { name = "M2: Cubical-Agda variant (Agda::cubical(), --cubical --safe island)", completion = 100 },
   { name = "M3: Flying-Logic reasoning graph (src/reason: And|Or juncts, demote-only cycle-safe Verdict propagation, additive studio JSON)", completion = 100 },
@@ -60,6 +60,16 @@ milestones = [
 # Remaining M0: `arghda doctor` Rust subcommand (interim: `just doctor` shells
 # the script's --verify-only table).
 #
+# M0 COMPLETED 2026-07-01: the `arghda doctor` subcommand lands, closing the
+# last M0 gap. Probes every known backend by running `<command> --version`;
+# reports runnable/detail honestly (runnable=false only when the binary truly
+# can't execute, never a guess). `Backend::probe()` (default over a new
+# `command()` method) + `Probe` type; `command()` distinguishes binary from
+# name (agda-cubical runs `agda`). `arghda doctor [--json]` + `just doctor`
+# repointed off the interim provision-script shim. Dogfooded here: 5/5 runnable
+# (agda 2.6.3, idris2 0.7.0, z3 4.8.12, cvc5 1.2.0; agda-cubical shares agda).
+# 108 tests.
+#
 # M2 landed 2026-07-01: Cubical-Agda variant. Implemented as a SEPARATE backend
 # `AgdaCubical` (name "agda-cubical") rather than the plan's `Agda::cubical()`
 # constructor — a distinct type expresses the flag-profile ISLAND better (a
@@ -152,10 +162,10 @@ milestones = [
 
 [critical-next-actions]
 actions = [
-  "M1 + M2 + M3 + M4 + M5 DONE. Five backends across both interaction models: agda, agda-cubical, idris2 (Assistant); z3, cvc5 (Solver). Next:",
-  "Finish M0: add the `arghda doctor` Rust subcommand — report which of the five backends are actually runnable (probe each binary), repoint `just doctor` at it, feed the Groove manifest. Closes the last M0 gap.",
-  "Flying-Logic epic M6: Lean4 adapter (lake build + #print axioms audit → honest Unknown soundness when the audit is absent). Lean 4.13.0 provisioned.",
-  "Flying-Logic epic M11: studio JSON freeze (reason/0.1) + Groove /.well-known/groove manifest (the one open v0.1 milestone).",
+  "M0 + M1 + M2 + M3 + M4 + M5 DONE. Five backends across both interaction models (agda, agda-cubical, idris2 Assistant; z3, cvc5 Solver) + reasoning graph + doctor. Engine spine core complete. Next:",
+  "Flying-Logic epic M6: Lean4 adapter (lake build + #print axioms audit → honest Unknown soundness when the audit is absent). Lean 4.13.0 provisioned. Sixth backend.",
+  "Flying-Logic epic M11: studio JSON freeze (reason/0.1) + Groove /.well-known/groove manifest (the one open v0.1 milestone; `arghda doctor` output feeds it).",
+  "Flying-Logic epic M7: Echidna dispatch seam (feature-gated client, same Outcome).",
   "M4 follow-on: .ipkg-declared roots; totality-hole (?name) + per-def `partial` lint.",
   "M3 follow-on: feed real verdicts into `reason` from a workspace `proven/` state + wire staleness from the content-hash closure (proven.rs).",
   "M8-M10 heavy tail (Coq/Rocq, Isabelle, Mizar) — gated on --heavy provisioning.",
@@ -167,9 +177,10 @@ 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-M2: 79 lib + 28 integration = 107 tests pass. Dogfooded via real CLI on
-# all five backends: agda + agda-cubical + idris2 (Assistant), z3 + cvc5
-# (Solver). Dogfooded historically against echo-types + agda-unused.
+# post-M0-doctor: 80 lib + 28 integration = 108 tests pass. `arghda doctor`
+# dogfooded: 5/5 backends runnable. All five backends dogfooded via real CLI:
+# agda + agda-cubical + idris2 (Assistant), z3 + cvc5 (Solver). Dogfooded
+# historically against echo-types + agda-unused.
 
 [ecosystem]
 part-of = ["arghda"]

Justfile

@@ -66,10 +66,9 @@ provision-heavy:
     bash scripts/provision-provers.sh --heavy
 
 # Report which prover/solver backends are actually runnable, no installs.
-# (Interim: shells the provision script's --verify-only table until the
-# `arghda doctor` subcommand lands.)
+# The `arghda doctor` subcommand probes each binary (`<tool> --version`).
 doctor:
-    bash scripts/provision-provers.sh --verify-only
+    cargo run --quiet -- doctor
 
 # RSR: the mandated machine-readable artefacts are present and well-formed.
 validate-rsr:

src/lib.rs

@@ -31,7 +31,7 @@ pub use event::{Event, EventKind};
 pub use graph::{build as build_graph, ImportGraph};
 pub use lint::{default_rules, rules_with_config, run_lints, LintRule, RuleConfig};
 pub use prover::{
-    default_backend, Agda, AgdaCubical, Backend, BackendKind, Idris2, Outcome, Smt, Verdict,
+    default_backend, Agda, AgdaCubical, Backend, BackendKind, Idris2, Outcome, Probe, Smt, Verdict,
 };
 pub use reason::{build as build_reason, Junct, ReasonDocument, ReasonEdge, ReasonNode};
 pub use workspace::{StaleEntry, State, Workspace};

src/main.rs

@@ -4,8 +4,8 @@
 use anyhow::{Context, Result};
 use arghda_core::lint::LintContext;
 use arghda_core::{
-    build_dag, build_reason, event, run_lints, unused, watcher, Agda, AgdaCubical, Backend, Idris2,
-    LintRule, RuleConfig, Smt, State, Workspace,
+    build_dag, build_reason, event, run_lints, unused, watcher, Agda, AgdaCubical, Backend,
+    BackendKind, Idris2, LintRule, RuleConfig, Smt, State, Workspace,
 };
 use clap::{Parser, Subcommand};
 use std::path::{Path, PathBuf};
@@ -15,6 +15,9 @@ use walkdir::WalkDir;
 /// A lint pack (boxed trait objects).
 type RuleSet = Vec<Box<dyn LintRule>>;
 
+/// Every backend `--backend` accepts and `doctor` probes.
+const KNOWN_BACKENDS: &[&str] = &["agda", "agda-cubical", "idris2", "z3", "cvc5"];
+
 /// Resolve a `--backend` name to a backend instance. Agda is the default and
 /// v0.1 reference; Idris2 is the estate ABI language.
 fn backend_for(name: &str) -> Result<Box<dyn Backend>> {
@@ -156,6 +159,12 @@ enum Cmd {
     },
     /// Watch `inbox/` and `working/` in a workspace; print events.
     Watch { workspace: PathBuf },
+    /// Probe which prover/solver backends are actually runnable here.
+    Doctor {
+        /// Emit the probe results as JSON.
+        #[arg(long)]
+        json: bool,
+    },
 }
 
 fn main() -> Result<()> {
@@ -237,6 +246,33 @@ fn main() -> Result<()> {
             invalidate,
         } => stale(&workspace, invalidate)?,
         Cmd::Watch { workspace } => watch(&workspace)?,
+        Cmd::Doctor { json } => doctor(json)?,
+    }
+    Ok(())
+}
+
+/// Probe every known backend and report which are actually runnable.
+fn doctor(json: bool) -> Result<()> {
+    let probes = KNOWN_BACKENDS
+        .iter()
+        .map(|name| backend_for(name).map(|b| b.probe()))
+        .collect::<Result<Vec<_>>>()?;
+
+    if json {
+        let payload = serde_json::json!({ "version": "0.1", "backends": probes });
+        println!("{}", serde_json::to_string_pretty(&payload)?);
+    } else {
+        println!("arghda doctor — backend availability");
+        for p in &probes {
+            let mark = if p.runnable { "OK" } else { "--" };
+            let kind = match p.kind {
+                BackendKind::Assistant => "assistant",
+                BackendKind::Solver => "solver",
+            };
+            println!("  [{mark}] {:<13} {:<10} {}", p.backend, kind, p.detail);
+        }
+        let runnable = probes.iter().filter(|p| p.runnable).count();
+        println!("\n{}/{} backends runnable", runnable, probes.len());
     }
     Ok(())
 }

src/prover/agda.rs

@@ -81,6 +81,10 @@ impl Backend for Agda {
     fn lint_rules(&self, cfg: &RuleConfig) -> Result<Vec<Box<dyn LintRule>>> {
         rules_with_config(cfg)
     }
+
+    fn command(&self) -> &'static str {
+        "agda"
+    }
 }
 
 impl Backend for AgdaCubical {
@@ -125,6 +129,11 @@ impl Backend for AgdaCubical {
     fn lint_rules(&self, cfg: &RuleConfig) -> Result<Vec<Box<dyn LintRule>>> {
         agda_cubical_rules(cfg)
     }
+
+    fn command(&self) -> &'static str {
+        // Same binary as standard Agda; the mode is the `--cubical` flag.
+        "agda"
+    }
 }
 
 /// Shared `agda` invocation for both flag profiles. `cubical` adds the
@@ -196,6 +205,20 @@ mod tests {
         assert_eq!(AgdaCubical.safe_mode(), Some("--cubical --safe"));
     }
 
+    #[test]
+    fn command_and_probe_are_honest() {
+        // Both Agda profiles run the same binary; the mode is a flag.
+        assert_eq!(Agda.command(), "agda");
+        assert_eq!(AgdaCubical.command(), "agda");
+        // probe() reports availability honestly, whether or not agda is here.
+        let p = Agda.probe();
+        assert_eq!(p.backend, "agda");
+        assert_eq!(p.kind, BackendKind::Assistant);
+        assert!(!p.detail.is_empty());
+        // agda-cubical probes the same binary, so agrees on runnability.
+        assert_eq!(AgdaCubical.probe().runnable, p.runnable);
+    }
+
     #[test]
     fn check_file_is_honest_about_availability() {
         // We cannot guarantee agda is absent in every environment, so we

src/prover/idris2.rs

@@ -149,6 +149,10 @@ impl Backend for Idris2 {
     fn lint_rules(&self, _cfg: &RuleConfig) -> Result<Vec<Box<dyn LintRule>>> {
         Ok(vec![Box::new(Idris2EscapeHatch)])
     }
+
+    fn command(&self) -> &'static str {
+        "idris2"
+    }
 }
 
 fn tail(s: &str, n: usize) -> String {

src/prover/mod.rs

@@ -25,6 +25,7 @@ use crate::lint::{LintRule, RuleConfig};
 use anyhow::Result;
 use serde::Serialize;
 use std::path::{Path, PathBuf};
+use std::process::Command;
 
 pub mod agda;
 pub mod idris2;
@@ -106,6 +107,55 @@ impl Outcome {
     }
 }
 
+/// The result of probing whether a backend's tool is actually runnable —
+/// the honest input to `arghda doctor`.
+#[derive(Clone, Debug, Serialize)]
+pub struct Probe {
+    /// The backend id (`agda`, `z3`, …).
+    pub backend: String,
+    /// Assistant or solver.
+    pub kind: BackendKind,
+    /// `true` iff the tool's binary could be executed.
+    pub runnable: bool,
+    /// The tool's version line, or why it is not runnable.
+    pub detail: String,
+}
+
+/// Probe a tool by running `<cmd> --version`. Reports `runnable` honestly:
+/// `false` only when the binary is absent / cannot be executed (never a
+/// guess). `detail` is the first output line, or the reason it failed.
+fn probe_tool(name: &str, kind: BackendKind, cmd: &str) -> Probe {
+    match Command::new(cmd).arg("--version").output() {
+        Ok(out) => {
+            let mut combined = String::from_utf8_lossy(&out.stdout).into_owned();
+            combined.push_str(&String::from_utf8_lossy(&out.stderr));
+            let first = combined.lines().next().unwrap_or("").trim().to_string();
+            Probe {
+                backend: name.to_string(),
+                kind,
+                runnable: true,
+                detail: if first.is_empty() {
+                    format!("ran `{cmd} --version`")
+                } else {
+                    first
+                },
+            }
+        }
+        Err(e) if e.kind() == std::io::ErrorKind::NotFound => Probe {
+            backend: name.to_string(),
+            kind,
+            runnable: false,
+            detail: format!("`{cmd}` not found on PATH"),
+        },
+        Err(e) => Probe {
+            backend: name.to_string(),
+            kind,
+            runnable: false,
+            detail: format!("`{cmd}` could not run: {e}"),
+        },
+    }
+}
+
 /// An object-safe adapter over one external prover or solver.
 ///
 /// Exactly the seams that used to be hardcoded to Agda live behind this
@@ -153,6 +203,17 @@ pub trait Backend: Send + Sync {
 
     /// The per-language lint pack, parameterised by operator config.
     fn lint_rules(&self, cfg: &RuleConfig) -> Result<Vec<Box<dyn LintRule>>>;
+
+    /// The external binary this backend shells out to (`agda`, `z3`, …).
+    /// May differ from [`Backend::name`] — e.g. `agda-cubical` runs `agda`.
+    fn command(&self) -> &'static str;
+
+    /// Probe whether the tool is actually runnable (for `arghda doctor`).
+    /// The default runs `<command> --version`; honest — `runnable` is false
+    /// only when the binary genuinely cannot be executed.
+    fn probe(&self) -> Probe {
+        probe_tool(self.name(), self.kind(), self.command())
+    }
 }
 
 /// The default backend when none is selected: Agda, the v0.1 language.

src/prover/smt.rs

@@ -129,6 +129,10 @@ impl Backend for Smt {
         // No source-level escape-hatch class for SMT-LIB2.
         Ok(Vec::new())
     }
+
+    fn command(&self) -> &'static str {
+        self.cmd
+    }
 }
 
 /// Map solver output + exit status to a [`Verdict`]. Parses the actual