ArghDA M8 follow-on: dependency-ordered Coq compilation (M8 → 97%) (#50)

## What

Multi-file Coq projects are now checkable. Before this, a bare `coqc
B.v` where `B` `Require`s an in-tree sibling `A` errored `Cannot find a
physical path bound to logical path A` (ground-truthed) — so any Coq
file with a local dependency verdicted `Error`.

## How

`check_file` now stages the target and its in-tree transitive `Require`
deps into a temp build tree, compiles the deps in **topological order**
(deps before dependents; `coq_transitive_deps` is a cycle-safe
post-order DFS) so each `.vo` exists, then checks the target against `-R
<build> ""`. It all happens under temp, so the source tree stays clean.
External stdlib/MML requires resolve on coqc's own load path (skipped as
non-in-tree).

## Honesty preserved — a transitive admit is NOT whitewashed

This is the load-bearing verification. Dogfooded: a dependent whose dep
contains `Admitted` gets a per-file `check` verdict of `proven` (the
dependent's own content is sound), **but the reasoning graph demotes its
EFFECTIVE verdict to `admitted`** via the And-edge to the admitted dep:

```
Bad      self=admitted   effective=admitted
UsesBad  self=proven     effective=admitted   (edge UsesBad → Bad)
```

So dep-ordering makes projects *checkable* without letting a transitive
admit ride through green — the self/effective split does its job.

## Verification (actually run)

- `cargo fmt --check` / `clippy -D warnings` — clean
- `cargo test` — **174 pass** (+1 topo-order unit)
- `check-spdx.sh` — OK

**Dogfooded vs real coqc 8.18.0:**

| case | result |
|---|---|
| `check C.v` in a 3-module `A ← B ← C` chain of real `Qed` proofs |
`proven` (was `error` before) |
| `reason --check` over the chain | A / B / C all `proven` |
| dependent of an `Admitted` module | per-file `proven`, **effective
`admitted`** |

## Scope

M8 → 97%. Residual: `_CoqProject`-driven custom `-Q`/`-R` prefix
remapping (the empty-prefix `Foo.Bar` ↔ `Foo/Bar.v` convention is fully
working; only non-default logical prefixes remain a follow-on).

Part of the heavy-tail completion cuts — next: Mizar prel export (M10),
then Isabelle multi-session (M9).

🤖 Generated with [Claude Code](https://claude.com/claude-code)

https://claude.ai/code/session_012MpYSh6Wy8YMBH2E3qVyT7

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

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

Author: hyperpolymath

.machine_readable/6a2/STATE.a2ml

@@ -48,7 +48,7 @@ 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 = 100 },
   { 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 = 90 },
+  { name = "M8: Coq/Rocq adapter (--heavy provisioning; Section-aware postulate classifier)", completion = 97 },
   { name = "M9: Isabelle adapter (--heavy; dogfood tropical-resource-typing .thy)", completion = 90 },
   { name = "M10: Mizar adapter (detect-only first; highest uncertainty)", completion = 85 },
   { name = "M11: studio JSON freeze (reason/0.1) + Groove manifest", completion = 100 },
@@ -114,6 +114,26 @@ milestones = [
 # --backend idris2` over an ipkg fixture → crt_roots ['App'], App+Helper wired.
 # M4 now 95% (remaining: totality-hole `?name` + per-def `partial` lint).
 #
+# M8 FOLLOW-ON landed 2026-07-01 (M8 90% → 97%): dependency-ordered Coq
+# compilation — multi-file projects are now checkable. Was: a bare `coqc B.v`
+# where B `Require`s an in-tree A errored "Cannot find a physical path bound to
+# logical path A" (ground-truthed). Now check_file stages the target + its
+# in-tree transitive `Require` deps into a temp build tree, compiles the deps in
+# TOPOLOGICAL order (deps before dependents; `coq_transitive_deps` = post-order
+# DFS, cycle-safe) so each `.vo` exists, then checks the target against `-R
+# <build> ""` — all under temp, source tree stays clean. External stdlib/MML
+# requires resolve on coqc's own load path (skipped as non-in-tree). CRUCIAL
+# honesty check (dogfooded): a dependent whose dep has an `Admitted` is NOT
+# whitewashed — per-file `check UsesBad.v` = proven (UsesBad's own content is
+# sound) but the reasoning graph demotes its EFFECTIVE verdict to admitted via
+# the And-edge to Bad (self=admitted). So dep-ordering makes projects checkable
+# WITHOUT letting a transitive admit ride through green — the self/effective
+# split does its job. 174 tests (+1 topo-order unit). Dogfooded vs real coqc
+# 8.18.0: a 3-module A←B←C chain of real Qed proofs → C=proven, reason --check
+# → A/B/C all proven. Residual 3%: `_CoqProject`-driven custom `-Q`/`-R` prefix
+# remapping (the empty-prefix `Foo.Bar`↔`Foo/Bar.v` convention is fully working;
+# only non-default logical prefixes remain a follow-on).
+#
 # M4 FOLLOW-ON landed 2026-07-01 (M4 → 100%): the Idris2 escape-hatch lint now
 # also flags a per-definition `partial` modifier (totality opt-out, distinct
 # from the already-handled file-wide `%default partial` directive) and totality
@@ -433,7 +453,7 @@ actions = [
   "M9 (Isabelle): DONE (90%) — Isabelle2025 provisioned + adapter built + dogfooded (proven/admitted/postulated/error) via session-build; ROOT-based roots, imports-clause edges. Remaining: session-qualified imports + dependency-ordered multi-session builds.",
   "M10 (Mizar): DONE (85%) — turned out to be a REAL verify, not detect-only: static i386 verifier runs on x86_64; provisioned + adapter (accom+verifier+.err) + dogfooded (proven/error). HEAVY TAIL M8-M10 COMPLETE. Remaining: local-article prel export.",
   "M7 client INVESTIGATED 2026-07-01 → BLOCKED (stub stays): no confirmed Echidna HTTP contract exists (dispatch.rs says API unconfirmed; ECOSYSTEM.a2ml gives no endpoints/schema; the echidna repo is out of this session's access scope). Building a client would mean inventing an unverifiable contract — forbidden. Unblock: a published Echidna API + a reachable instance to dogfood; then wire Dispatch::run behind a cargo feature. ROADMAP TERMINUS — all tractable items done; M7's client is the sole residual, externally blocked.",
-  "Deeper cuts deliberately scoped out (available if the owner wants them): Coq _CoqProject logical-path resolution + dependency-ordered compilation; Mizar local-article prel export (miz2prel); Isabelle session-qualified imports + multi-session builds; and the arghda-studio visual layer that consumes the frozen reason/0.1 JSON.",
+  "HEAVY-TAIL COMPLETION CUTS (owner asked for these 2026-07-01, doing foundation-first, one PR each, real-tool dogfood): [DONE] Coq dependency-ordered compilation (M8 90→97%); [NEXT] Mizar local-article prel export via miz2prel so cross-article refs check (M10 85→~100%); [THEN] Isabelle session-qualified imports + multi-session builds (M9 90→~100%). Residual after: Coq _CoqProject custom -Q/-R prefixes (3%); arghda-studio visual layer (separate repo, out of this session's scope; AffineScript).",
 ]
 
 [maintenance-status]
@@ -442,8 +462,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-M4-followon: 130 lib + 43 integration = 173 tests pass. M4 totality-hole
-# + partial lint dogfooded vs real idris2 0.7.0 (green --check capped to amber).
+# post-M8-deporder: 131 lib + 43 integration = 174 tests pass. M8 dependency-
+# ordered Coq compilation dogfooded vs real coqc 8.18.0 (A←B←C chain → all
+# proven; transitive admit demotes the dependent's effective verdict, not
+# whitewashed). M4 totality-hole + partial lint dogfooded vs real idris2 0.7.0.
 # M6 lake-env import resolution dogfooded vs real Lean 4.13.0 + Lake 5.0.0
 # (imported file in a built lake project → proven; outside → error). codeql.yml added
 # (code-scanning gate fix). M10 Mizar adapter dogfooded vs real Mizar 8.1.15

src/prover/rocq.rs

@@ -9,8 +9,9 @@
 //! that declares `Axiom`/`Parameter`/`Conjecture` postulates — all exit 0.
 //! So the honest verdict, ground-truthed against Coq 8.18.0, is:
 //! * exit non-zero → [`Verdict::Error`] (the kernel rejected something, or an
-//!   import could not be resolved — a bare single-file `coqc` cannot build a
-//!   dependency chain; that is a documented limitation, not a proof).
+//!   in-tree dependency failed to build — see the dependency-ordered build
+//!   below; a genuinely unresolved external import is an honest error, not a
+//!   proof).
 //! * exit 0, source contains `Admitted`/`admit` → [`Verdict::Admitted`] (an
 //!   unfinished proof rode along on a green compile).
 //! * exit 0, source contains a genuine unverified postulate → [`Verdict::Postulated`].
@@ -34,10 +35,14 @@
 //! Import edges come only from `Require` (with or without `Import`/`Export`,
 //! and the `From P Require …` form); a bare `Import`/`Export` is a namespace
 //! directive, not a dependency edge (as Lean's `open` is), so it is ignored.
-//! `_CoqProject`-driven logical-path resolution and dependency-ordered
-//! compilation are documented follow-ons; this baseline compiles a single
-//! file with `-R <root> ""` and honestly reports `Error` when a dependency it
-//! cannot build is required.
+//! Dependency-ordered compilation: [`Backend::check_file`] stages the target
+//! and its in-tree transitive `Require` deps into a temp build tree, compiles
+//! the deps in topological order (so each `Require`d sibling has its `.vo`),
+//! then checks the target against the same load path — all under temp, so the
+//! source tree stays clean. External (stdlib/MML) requires resolve on coqc's
+//! own load path. `_CoqProject`-driven logical-path remapping (custom `-Q`/`-R`
+//! prefixes) remains a documented follow-on; this uses the empty-prefix
+//! convention (`Foo.Bar` ↔ `Foo/Bar.v` under the root).
 
 use super::{Backend, BackendKind, Outcome, Verdict};
 use crate::graph;
@@ -76,39 +81,61 @@ impl Backend for Coq {
     }
 
     fn check_file(&self, file: &Path, include_root: &Path) -> Result<Outcome> {
-        // Redirect the compiled `.vo` into a temp *directory* so the source
-        // tree stays clean, and map the include root to the empty logical
-        // prefix so a sibling `Require` at least has a chance to resolve.
-        // `coqc -o` insists the target basename equal the source's (only the
-        // directory may differ), so keep the stem and vary the directory.
+        // Stage the target and its in-tree `Require` dependencies into a temp
+        // build tree, compile the deps in topological order (deps before
+        // dependents) so each `Require`d sibling has its `.vo`, then check the
+        // target against the same load path. The whole build happens under
+        // temp, so the source tree stays clean. External (stdlib/MML) requires
+        // are left for coqc's own load path.
+        let src = fs::read_to_string(file).unwrap_or_default();
         let nanos = SystemTime::now()
             .duration_since(UNIX_EPOCH)
             .map(|d| d.as_nanos())
             .unwrap_or(0);
-        let out_dir =
+        let build =
             std::env::temp_dir().join(format!("arghda-coq-{}-{}", std::process::id(), nanos));
-        let _ = fs::create_dir_all(&out_dir);
-        let stem = file.file_stem().and_then(|s| s.to_str()).unwrap_or("Check");
-        let vo_out = out_dir.join(format!("{stem}.vo"));
-
-        let output = Command::new("coqc")
-            .arg("-q") // ignore any coqrc
-            .arg("-no-glob") // don't drop a .glob next to the source
-            .arg("-R")
-            .arg(include_root)
-            .arg("")
-            .arg("-o")
-            .arg(&vo_out)
-            .arg(file)
-            .output();
-
-        let _ = fs::remove_dir_all(&out_dir);
+        if fs::create_dir_all(&build).is_err() {
+            return Ok(Outcome::unavailable(BackendKind::Assistant));
+        }
+
+        // The target's module name (relative to the include root), and its
+        // in-tree transitive Require deps in dependency-first order.
+        let target_module = self.module_name_of(file, include_root).unwrap_or_else(|| {
+            file.file_stem()
+                .and_then(|s| s.to_str())
+                .unwrap_or("Check")
+                .into()
+        });
+        let deps = coq_transitive_deps(&parse_requires(&src), include_root);
+
+        // Stage every dep + the target into the build tree at its module path.
+        for m in &deps {
+            let dst = coq_module_path(m, &build);
+            if let Some(parent) = dst.parent() {
+                let _ = fs::create_dir_all(parent);
+            }
+            let _ = fs::copy(coq_module_path(m, include_root), dst);
+        }
+        let target_dst = coq_module_path(&target_module, &build);
+        if let Some(parent) = target_dst.parent() {
+            let _ = fs::create_dir_all(parent);
+        }
+        let _ = fs::copy(file, &target_dst);
+
+        // Compile the deps first (best-effort: a dep that fails to build
+        // surfaces honestly as a `Require` error when the target is checked).
+        for m in &deps {
+            let _ = coqc_build(&coq_module_path(m, &build), &build);
+        }
+
+        // Check the target against the built deps.
+        let output = coqc_build(&target_dst, &build);
+        let _ = fs::remove_dir_all(&build);
 
         match output {
             Ok(out) => {
                 let mut combined = String::from_utf8_lossy(&out.stdout).into_owned();
                 combined.push_str(&String::from_utf8_lossy(&out.stderr));
-                let src = fs::read_to_string(file).unwrap_or_default();
                 let verdict = coq_verdict(&src, out.status.success());
                 Ok(Outcome {
                     available: true,
@@ -131,12 +158,7 @@ impl Backend for Coq {
     }
 
     fn module_to_path(&self, module: &str, include_root: &Path) -> PathBuf {
-        let mut p = include_root.to_path_buf();
-        for part in module.split('.') {
-            p.push(part);
-        }
-        p.set_extension("v");
-        p
+        coq_module_path(module, include_root)
     }
 
     fn direct_imports(&self, file: &Path) -> Result<Vec<String>> {
@@ -175,6 +197,65 @@ impl Backend for Coq {
     }
 }
 
+/// Dotted Coq logical name → file path under `root` (`Foo.Bar` → `Foo/Bar.v`).
+fn coq_module_path(module: &str, root: &Path) -> PathBuf {
+    let mut p = root.to_path_buf();
+    for part in module.split('.') {
+        p.push(part);
+    }
+    p.set_extension("v");
+    p
+}
+
+/// Compile one staged `.v` under the build tree, mapping the build root to the
+/// empty logical prefix so in-tree `Require`s resolve against the `.vo`s built
+/// alongside. `-no-glob` keeps the tree free of `.glob` output.
+fn coqc_build(file: &Path, build_root: &Path) -> std::io::Result<std::process::Output> {
+    Command::new("coqc")
+        .arg("-q")
+        .arg("-no-glob")
+        .arg("-R")
+        .arg(build_root)
+        .arg("")
+        .arg(file)
+        .output()
+}
+
+/// The in-tree transitive `Require` dependencies of a file, given its direct
+/// imports, in dependency-first (topological) order — deps appear before the
+/// modules that require them, so compiling the list left-to-right satisfies
+/// every `Require`. External modules (stdlib/MML, absent under `include_root`)
+/// are skipped. Cycle-safe via the visited set (Coq forbids import cycles, but
+/// a half-edited file could transiently produce one).
+fn coq_transitive_deps(direct: &[String], include_root: &Path) -> Vec<String> {
+    let mut visited = std::collections::HashSet::new();
+    let mut order = Vec::new();
+    for m in direct {
+        coq_visit_dep(m, include_root, &mut visited, &mut order);
+    }
+    order
+}
+
+fn coq_visit_dep(
+    module: &str,
+    include_root: &Path,
+    visited: &mut std::collections::HashSet<String>,
+    order: &mut Vec<String>,
+) {
+    if !visited.insert(module.to_string()) {
+        return;
+    }
+    // Only in-tree modules resolve to a readable file; external ones are left
+    // for coqc's own load path.
+    let Ok(src) = fs::read_to_string(coq_module_path(module, include_root)) else {
+        return;
+    };
+    for imp in parse_requires(&src) {
+        coq_visit_dep(&imp, include_root, visited, order);
+    }
+    order.push(module.to_string());
+}
+
 /// Map Coq source + exit status to a [`Verdict`], honestly: a green compile is
 /// `Proven` (the kernel checked every `Qed`) *unless* an escape hatch is
 /// present — `Admitted`/`admit` ⇒ `Admitted`, a genuine postulate ⇒
@@ -524,6 +605,25 @@ End OrderedField.\n";
         assert_eq!(count_genuine_postulates("Parameter foo.\n"), 1);
     }
 
+    #[test]
+    fn transitive_deps_are_topologically_ordered() {
+        // C requires B; B requires A; A is a leaf. The build order for C must
+        // be [A, B] (deps before dependents); external requires are skipped.
+        let tmp = tempfile::tempdir().unwrap();
+        let r = tmp.path();
+        std::fs::write(r.join("A.v"), "Definition a : nat := 0.\n").unwrap();
+        std::fs::write(r.join("B.v"), "Require Import A.\nDefinition b := a.\n").unwrap();
+        std::fs::write(
+            r.join("C.v"),
+            "Require Import B.\nRequire Import Coq.Lists.List.\nDefinition c := b.\n",
+        )
+        .unwrap();
+        let deps = coq_transitive_deps(&parse_requires("Require Import B.\n"), r);
+        assert_eq!(deps, vec!["A".to_string(), "B".to_string()]);
+        // The external stdlib require is not staged as an in-tree dep.
+        assert!(!deps.iter().any(|m| m.contains("List")));
+    }
+
     #[test]
     fn check_file_is_honest_about_availability() {
         let tmp = tempfile::tempdir().unwrap();