ArghDA M0 complete: arghda doctor — honest backend availability probe

[hyperpolymath]

What & why

Closes the last M0 gap. arghda doctor probes every known backend by running <command> --version and reports which are actually runnable — honestly (runnable=false only when the binary genuinely cannot execute, never a guess), the same discipline as check_file's graceful degradation.

Changes

• src/prover/mod.rs — Probe { backend, kind, runnable, detail } + probe_tool(); Backend::command() (the binary, which may differ from name() — agda-cubical runs agda) + a default Backend::probe().
• src/prover/{agda,idris2,smt}.rs — command() for each of the five backends.
• src/main.rs — doctor [--json] subcommand over KNOWN_BACKENDS.
• Justfile — just doctor repointed off the interim provision-script shim onto cargo run -- doctor.

Verified (ran, not inferred)

• cargo test → 108 passing, 0 failed (+1 probe/command honesty unit).
• cargo clippy -D warnings clean · cargo fmt --check clean · check-spdx.sh OK.
• Dogfooded arghda doctor → 5/5 runnable, real version lines:

  [OK] agda          assistant  Agda version 2.6.3
  [OK] agda-cubical  assistant  Agda version 2.6.3
  [OK] idris2        assistant  Idris 2, version 0.7.0
  [OK] z3            solver     Z3 version 4.8.12 - 64 bit
  [OK] cvc5          solver     This is cvc5 version 1.2.0 …
  

  --json emits the machine-readable form.

Milestone status

Engine-spine core (M0–M5) complete. Five backends across both interaction models, the Flying-Logic reasoning graph, and now a discovery command. Next: M6 (Lean4), M11 (studio JSON freeze + Groove manifest — doctor output feeds it).

---

Generated by Claude Code