ArghDA → Flying Logic for provers/solvers: M0 (toolchain provisioning + doctor) (#31)

## Context

First increment of the epic to evolve `arghda-core` from 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 reported `OK` only when its own
`--version` returned 0 in the run; everything else prints as
`MISSING`/`FAILED` with the command tried. Third-party sources are
fetched as **curl tarballs, not `git clone`** — the environment's proxy
403s git-relay access to non-scoped repos, and tarballs are more
portable anyway.

**`Justfile`** — `provision` / `provision-heavy` / `doctor` recipes
(interim `doctor` shells the script's `--verify-only` table until the
`arghda doctor` Rust subcommand lands).

**`scripts/check-spdx.sh` + `licensing-policy.toml`** — ⚠️
*licence-adjacent, flagged for review.* Fixes a pre-existing checker
bug: the prose SPDX variable was `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 failing `just
license-check` on 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 canonical `LICENSES/` 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 `--version` output)

| Backend | Result |
|---|---|
| Agda | ✅ 2.6.3 (+ stdlib v2.3 + cubical library + `--cubical` flag) |
| Zig | ✅ 0.15.2 |
| Z3 | ✅ 4.8.12 |
| CVC5 | ✅ 1.2.0 |
| Lean 4 | ✅ 4.13.0 |
| Idris2 | building via chez bootstrap (ABI-language priority) |
| Coq/Rocq, Isabelle, Mizar | scripted behind `--heavy`/`--mizar`; not
installed this session |

`just check` passes (fmt + clippy `-D warnings` + SPDX + build + **64
tests, 0 failed**).

## Next (not in this PR)

M1 — the keystone: introduce a `Backend` trait spanning two kinds
(proof-assistant `Assistant` typecheck→exit-code; `Solver`
SMT-LIB2→sat/unsat/unknown) with a common `Verdict` enum, move `agda.rs`
behind 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](https://claude.com/claude-code)

---
_Generated by [Claude
Code](https://claude.ai/code/session_012MpYSh6Wy8YMBH2E3qVyT7)_

---------

Co-authored-by: Claude <noreply@anthropic.com>

Author: hyperpolymath

.machine_readable/6a2/STATE.a2ml

@@ -6,7 +6,7 @@
 [metadata]
 project = "arghda-core"
 version = "0.1.0"
-last-updated = "2026-06-20"
+last-updated = "2026-07-01"
 status = "active"  # active | paused | archived
 
 [project-context]
@@ -33,17 +33,50 @@ milestones = [
   { name = "Groove service manifest (/.well-known/groove) for PanLL discovery", completion = 0 },
 ]
 
+# "Flying Logic for provers/solvers" epic (v0.2+): generalise the Agda-only
+# engine into a multi-backend reasoning-graph workspace. Two backend kinds:
+# proof-assistants (typecheck a file -> exit code) and solvers (SMT-LIB2 ->
+# sat/unsat/unknown). Backends shell out to real binaries; a node is only
+# "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 = "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 = 0 },
+  { name = "M2: Cubical-Agda variant (Agda::cubical(), --cubical --safe island)", completion = 0 },
+  { name = "M3: Flying-Logic reasoning graph (src/reason: And|Or juncts, demote-only cycle-safe Verdict propagation, additive studio JSON)", completion = 0 },
+  { name = "M4: Idris2 adapter (core/ABI language: .ipkg/--check/totality; escape-hatches)", completion = 0 },
+  { name = "M5: SMT solver backends (Z3, CVC5): SMT-LIB2 -> sat/unsat/unknown -> Verdict", completion = 0 },
+  { name = "M6: Lean4 adapter (lake build + #print axioms audit)", completion = 0 },
+  { name = "M7: Echidna dispatch seam (optional route to orchestrator :8090, same Outcome)", completion = 0 },
+  { name = "M8: Coq/Rocq adapter (--heavy provisioning; Section-aware postulate classifier)", completion = 0 },
+  { 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 = 0 },
+]
+# 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.
+# Remaining M0: `arghda doctor` Rust subcommand (interim: `just doctor` shells
+# the script's --verify-only table).
+
 [blockers-and-issues]
 # No active blockers. v0.1 lint set + DAG schema (arghda-spec.adoc) are
 # complete. The SPDX licence invariant is applied and enforced
 # (scripts/check-spdx.sh; .machine_readable/licensing-policy.toml).
+# 2026-07-01: fixed a pre-existing checker bug — check-spdx.sh's prose variable
+# was set to MPL-2.0, contradicting the declared policy (prose = CC-BY-SA-4.0 in
+# licensing-policy.toml) and the checker's own failure label; it now matches
+# the declaration. NO licence header on any file changed; the LICENSES/ REUSE
+# dir is now excluded (canonical texts). This was blocking `just license-check`.
 
 [critical-next-actions]
 actions = [
-  "Template-applicability: rsr-profile.a2ml declares capabilities (landed); estate policy + gate model + reference checker landed in hyperpolymath/standards#391 + #392 (pure capability-gating). Follow-up: wire the standards rsr-profile check into CI.",
-  "Transitive-import closure hashing landed (workspace [proven] include_root); follow-up: also expose it as a --include-root CLI flag on promote/stale.",
-  "Serve /.well-known/groove for PanLL discovery (Groove protocol)",
-  "Scaffold arghda-studio (AffineScript visual layer consuming the dag JSON)",
+  "Flying-Logic epic M1: introduce the Backend trait (Assistant|Solver) and move agda.rs to prover/agda.rs as a PURE REFACTOR — the 50 existing tests are the oracle, they must stay green with no behaviour change. This is the keystone everything else rides on.",
+  "Flying-Logic epic M3: src/reason reasoning graph (And|Or juncts + demote-only cycle-safe Verdict propagation) — independent of new backends, lands the headline capability early.",
+  "Finish M0: add the `arghda doctor` Rust subcommand and repoint `just doctor` at it (interim shells provision-provers.sh --verify-only).",
+  "Transitive-import closure hashing landed; follow-up: expose it as a --include-root CLI flag on promote/stale.",
+  "Serve /.well-known/groove for PanLL discovery (Groove protocol) — folds into M11.",
 ]
 
 [maintenance-status]

.machine_readable/licensing-policy.toml

@@ -22,6 +22,7 @@ prose = "CC-BY-SA-4.0"  # *.adoc, *.md narrative
 paths = [
   "Cargo.lock",      # generated by cargo; enumerates third-party dependencies
   "LICENSE",         # the MPL-2.0 licence text itself
+  "LICENSES/",       # canonical SPDX licence texts (REUSE dir: MPL-2.0 + CC-BY-SA-4.0)
   "target/",         # cargo build output (gitignored)
   "tests/fixtures/", # Agda test-input data (some deliberately malformed)
 ]

Justfile

@@ -55,6 +55,22 @@ dag path:
 agda-check file:
     cargo run -- check "{{file}}"
 
+# Provision the prover/solver toolchains ArghDA drives (tractable set:
+# agda+cubical, zig, idris2, lean4, z3, cvc5). Honest: a backend is reported
+# OK only if its own --version actually returned 0 in the run.
+provision:
+    bash scripts/provision-provers.sh
+
+# As `provision`, plus the heavy backends (Coq via opam, Isabelle ~4 GB).
+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.)
+doctor:
+    bash scripts/provision-provers.sh --verify-only
+
 # RSR: the mandated machine-readable artefacts are present and well-formed.
 validate-rsr:
     @for f in STATE META ECOSYSTEM AGENTIC NEUROSYM PLAYBOOK; do \

scripts/check-spdx.sh

@@ -5,7 +5,7 @@
 # Licence invariant for arghda-core (enforced by `just check` + Rust CI).
 #
 #   code / config / scripts / state   ->  SPDX-License-Identifier: MPL-2.0
-#   prose documentation (*.adoc, *.md) ->  SPDX-License-Identifier: MPL-2.0
+#   prose documentation (*.adoc, *.md) ->  SPDX-License-Identifier: CC-BY-SA-4.0
 #
 # Files that are NOT ours, generated, or test-input data are EXCLUDED and must
 # never carry the repo's licence choices. The machine-readable declaration of
@@ -20,13 +20,14 @@ set -euo pipefail
 cd "$(git rev-parse --show-toplevel)"
 
 MPL='SPDX-License-Identifier: MPL-2.0'
-CC='SPDX-License-Identifier: MPL-2.0'
+CC='SPDX-License-Identifier: CC-BY-SA-4.0'
 fail=0
 
 # Not ours / generated / test-input data — see [excluded] in the policy file.
 excluded() {
   case "$1" in
     Cargo.lock | LICENSE) return 0 ;;          # generated lockfile / the licence text itself
+    LICENSES/*) return 0 ;;                     # canonical SPDX licence texts (REUSE dir)
     target/* | tests/fixtures/*) return 0 ;;   # build output / Agda test-input data
     *) return 1 ;;
   esac