Skip to content

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
hyperpolymath merged 1 commit into from
Jul 17, 2026
Merged

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

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
30 changes: 26 additions & 4 deletions .machine_readable/6a2/STATE.a2ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 },
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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]
Expand All @@ -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
Expand Down
170 changes: 135 additions & 35 deletions src/prover/rocq.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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`].
Expand All @@ -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;
Expand Down Expand Up @@ -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,
Expand All @@ -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>> {
Expand Down Expand Up @@ -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 ⇒
Expand Down Expand Up @@ -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();
Expand Down
Loading