From a3b06f8ea70576cdf491c6e8bafd079a4bfb984e Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 16 Jul 2026 22:51:14 +0000 Subject: [PATCH] =?UTF-8?q?ArghDA=20M8=20follow-on:=20dependency-ordered?= =?UTF-8?q?=20Coq=20compilation=20(M8=20=E2=86=92=2097%)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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. 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 ""`. It all happens under temp, so the source tree stays clean. External stdlib/MML requires resolve on coqc's own load path (they're skipped as non-in-tree). Honesty preserved — a transitive admit is NOT whitewashed. 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. 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, cargo test (174 pass, +1 topo-order unit), check-spdx.sh — all green. Dogfooded vs real coqc 8.18.0: a 3-module A←B←C chain of real Qed proofs → `check C.v` = proven; `reason --check` → A/B/C all proven; the admit-taint case demotes as above. Residual (the 3%): `_CoqProject`-driven custom `-Q`/`-R` prefix remapping. The empty-prefix convention (`Foo.Bar` ↔ `Foo/Bar.v` under the root) is fully working; only non-default logical prefixes remain a follow-on. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_012MpYSh6Wy8YMBH2E3qVyT7 --- .machine_readable/6a2/STATE.a2ml | 30 +++++- src/prover/rocq.rs | 170 ++++++++++++++++++++++++------- 2 files changed, 161 insertions(+), 39 deletions(-) diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index 6b3e51e..7c19443 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.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 +# ""` — 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 diff --git a/src/prover/rocq.rs b/src/prover/rocq.rs index c3aaa1a..eb5f4c6 100644 --- a/src/prover/rocq.rs +++ b/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 ""` 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 { - // 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> { @@ -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 { + 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 { + 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, + order: &mut Vec, +) { + 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();