diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index 32de7ba..d0cd8a8 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -11,7 +11,7 @@ status = "active" # active | paused | archived [project-context] name = "arghda-core" -purpose = "Multi-backend proof-workspace manager — the 'Flying Logic for provers/solvers' engine. A four-state triage workspace (inbox/working/proven/rejected) as file moves, per-backend lint packs targeting the silent-failure class, a backend-parametric import-graph DAG, a demote-only status-propagating reasoning graph, and a JSON + event-stream contract a visual layer (arghda-studio) consumes. Six backends across both interaction models (Agda, Cubical-Agda, Idris2, Lean4 assistants; Z3, CVC5 solvers). It never proves anything itself; the tools do." +purpose = "Multi-backend proof-workspace manager — the 'Flying Logic for provers/solvers' engine. A four-state triage workspace (inbox/working/proven/rejected) as file moves, per-backend lint packs targeting the silent-failure class, a backend-parametric import-graph DAG, a demote-only status-propagating reasoning graph, and a JSON + event-stream contract a visual layer (arghda-studio) consumes. Seven backends across both interaction models (Agda, Cubical-Agda, Idris2, Lean4, Coq/Rocq assistants; Z3, CVC5 solvers). It never proves anything itself; the tools do." completion-percentage = 92 [position] @@ -48,15 +48,18 @@ 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 = 92 }, { 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 = 0 }, + { name = "M8: Coq/Rocq adapter (--heavy provisioning; Section-aware postulate classifier)", completion = 90 }, { 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 = 100 }, ] # 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. +# real --version. idris2 v0.7.0 builds via chez bootstrap. COQ NOW INSTALLED +# (2026-07-01, heavy-tail foundation): opam 2.1.5 via apt → `opam install +# coq.8.18.0` → coqc reports real --version; symlinked to /usr/local/bin/coqc +# so `arghda doctor` probes it ([OK] coq assistant). Isabelle/Mizar remain +# 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). # @@ -116,6 +119,36 @@ milestones = [ # proven root → unknown; edit the proven file on disk → Good demoted to unknown # with the stale evidence string. M3 base was 100%; this is pure additive refinement. # +# M8 landed 2026-07-01 (90%, first heavy-tail backend): the Coq/Rocq adapter. +# Foundation-first — provisioned coqc 8.18.0 (opam) BEFORE the adapter, then +# built + dogfooded against the REAL tool. src/prover/rocq.rs (`Coq`): Assistant +# kind, extensions [v], command `coqc`. Verdict logic, ground-truthed vs Coq +# 8.18.0: exit≠0 → Error; exit 0 + `Admitted`/`admit` → Admitted; exit 0 + +# genuine postulate → Postulated; exit 0 clean → Proven (coqc kernel-checks +# every `Qed` at compile, so this is honest — stronger than Lean's need for a +# #print axioms audit). "Genuine postulate" = `count_genuine_postulates`, the +# Section-aware classifier PORTED from panic-attack's +# `count_rocq_unverified_postulates`: Section-scoped Variable/Hypothesis/ +# Parameter discharge at End; module-level Parameter of carrier/decidability/ +# non-Prop-function type are abstractions; Prop-valued Axiom/Parameter counted. +# check_file redirects the .vo to a temp DIR keeping the source stem (coqc `-o` +# insists target basename == source; a REAL-coqc dogfood caught my first +# attempt renaming it). Imports: `Require [Import|Export]` + `From P Require …` +# (bare Import/Export = namespace directive, not an edge, like Lean `open`). +# Roots: `All.v` aggregator convention (mirrors Agda). Lint: src/lint/coq.rs +# `CoqEscapeHatch` (warn, shared name `escape-hatch`) flags Admitted/admit/ +# Axiom/Conjecture (Parameter left to the backend classifier). Wired: backend_for +# "coq" + KNOWN_BACKENDS + all four `--backend` help strings + about line. +# 146 tests (+7 rocq unit +5 coq lint unit +3 coq integration; graph tests +# hermetic — text only, run tool-less). DOGFOODED vs real coqc 8.18.0: check +# → Clean=proven / Admits=admitted / Postulate=postulated / Broken=error; +# `reason --check --backend coq` reproduces those; import edge All→Base parsed, +# All.v discovered as crt_root, Base+Util wired, Orphan unwired; `doctor` → +# [OK] coq assistant 8.18.0. Remaining 10%: `_CoqProject`-driven logical-path +# resolution + dependency-ordered compilation (a bare single-file coqc reports +# Error when an uncompiled dependency is Required — documented limitation, same +# class as Lean's lake-env gap). +# # M7 landed 2026-07-01 (70%): the Echidna dispatch seam — completes the # engine-spine deliverable (M0-M7 + M11). src/dispatch.rs: `Dispatch { Local, # Echidna { base_url } }` + `run(backend, file, include_root) -> Outcome` @@ -277,7 +310,8 @@ actions = [ "M6 follow-on: #print axioms audit DONE (import-free files promote honestly); remaining = lake-env/LEAN_PATH so imported files can be checked + audited too.", "M4 follow-on: .ipkg-declared roots DONE; remaining = totality-hole (?name) + per-def `partial` lint.", "M3 follow-on: DONE — `reason --workspace ` sources real verdicts from a `proven/` state (workspace_verdicts) + demotes stale-proven via the content-hash closure. Refinement follow-ons bucket now complete.", - "M8-M10 heavy tail (Coq/Rocq, Isabelle, Mizar) — gated on --heavy provisioning (Coq via opam ~1hr; Isabelle ~4GB; Mizar niche).", + "M8 (Coq/Rocq): DONE (90%) — coqc 8.18.0 provisioned + adapter built + dogfooded (proven/admitted/postulated/error) with Section-aware postulate classifier. Remaining: _CoqProject logical paths + dependency-ordered compilation.", + "M9-M10 heavy tail (Isabelle, Mizar) — next, foundation-first: Isabelle ~4GB tarball then adapter; Mizar niche/detect-only. Then climb to M6 lake-env, M4 totality lint, M7 Echidna client.", ] [maintenance-status] @@ -286,13 +320,13 @@ 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-M3-followon: 96 lib + 34 integration = 130 tests pass. codeql.yml added -# (code-scanning gate fix). reason --workspace verdicts+staleness dogfooded. -# Lean #print axioms audit dogfooded. doctor/groove/dispatch -# dogfooded: 6/6 backends runnable; groove writes /.well-known/groove; --dispatch -# local real, echidna honest-stub. All six backends dogfooded via real CLI: agda -# + agda-cubical + idris2 + lean4 (Assistant), z3 + cvc5 (Solver). Dogfooded -# historically vs echo-types + agda-unused. +# post-M8: 108 lib + 38 integration = 146 tests pass. codeql.yml added +# (code-scanning gate fix). M8 Coq adapter dogfooded vs real coqc 8.18.0 +# (proven/admitted/postulated/error; reason --check; import edges; roots; wired; +# doctor [OK] coq). reason --workspace verdicts+staleness dogfooded. Lean +# #print axioms audit dogfooded. doctor/groove/dispatch dogfooded. SEVEN +# backends now: agda + agda-cubical + idris2 + lean4 + coq (Assistant), z3 + +# cvc5 (Solver). Dogfooded historically vs echo-types + agda-unused. [ecosystem] part-of = ["arghda"] diff --git a/src/lib.rs b/src/lib.rs index 0def871..22158f8 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -35,8 +35,8 @@ pub use graph::{build as build_graph, ImportGraph}; pub use groove::{manifest as groove_manifest, GrooveManifest}; pub use lint::{default_rules, rules_with_config, run_lints, LintRule, RuleConfig}; pub use prover::{ - default_backend, Agda, AgdaCubical, Backend, BackendKind, Idris2, Lean, Outcome, Probe, Smt, - Verdict, + default_backend, Agda, AgdaCubical, Backend, BackendKind, Coq, Idris2, Lean, Outcome, Probe, + Smt, Verdict, }; pub use reason::{ build as build_reason, workspace_verdicts, Junct, ReasonDocument, ReasonEdge, ReasonNode, diff --git a/src/lint/coq.rs b/src/lint/coq.rs new file mode 100644 index 0000000..f4cf032 --- /dev/null +++ b/src/lint/coq.rs @@ -0,0 +1,154 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) + +//! Coq / Rocq `escape-hatch` (warn) — surface soundness escape hatches. +//! +//! The Coq analogue of the Agda/Idris2/Lean escape-hatch rules; shares the +//! rule *name* `escape-hatch` so the reasoning graph caps any hit at amber. +//! +//! Flags the unambiguous holes: `Admitted`/`admit` (a proof closed as an +//! axiom / left as a placeholder) and `Axiom`/`Conjecture` (declared, not +//! proved). `coqc` compiles all of these with exit 0, so without this warn — +//! and without the backend's Section-aware postulate classification — they +//! ride along invisibly. `Parameter`/`Variable`/`Hypothesis` are deliberately +//! NOT flagged here: they are legitimate scaffold shapes far more often than +//! not, and the genuine module-level `Parameter` postulate is caught by the +//! backend's `count_genuine_postulates` (Section-aware) instead. + +use super::{LintContext, LintRule}; +use crate::diagnostic::{Diagnostic, LintReport, Severity}; +use anyhow::{Context, Result}; +use std::fs; +use std::path::Path; + +pub struct CoqEscapeHatch; + +const ESCAPE_TOKENS: &[&str] = &["Admitted", "admit", "Axiom", "Conjecture"]; + +impl LintRule for CoqEscapeHatch { + fn name(&self) -> &'static str { + "escape-hatch" + } + + fn run(&self, file: &Path, _ctx: &LintContext<'_>, report: &mut LintReport) -> Result<()> { + let contents = + fs::read_to_string(file).with_context(|| format!("reading {}", file.display()))?; + for (i, raw) in contents.lines().enumerate() { + let trimmed = raw.trim_start(); + if trimmed.starts_with("(*") { + continue; // whole-line comment (common case) + } + let code = strip_line_comments(raw); + for tok in ESCAPE_TOKENS { + if has_token(&code, tok) { + report.push(warn( + self.name(), + file, + i + 1, + format!("escape primitive `{tok}`"), + )); + } + } + } + Ok(()) + } +} + +fn warn(rule: &str, file: &Path, line: usize, message: String) -> Diagnostic { + Diagnostic { + rule: rule.to_string(), + severity: Severity::Warn, + file: file.to_path_buf(), + message, + line: Some(line), + } +} + +/// Remove balanced `(* … *)` spans; an unmatched `(*` truncates the rest of +/// the line. +fn strip_line_comments(line: &str) -> String { + let mut out = String::with_capacity(line.len()); + let bytes = line.as_bytes(); + let mut i = 0; + let mut depth = 0u32; + while i < bytes.len() { + if i + 1 < bytes.len() && bytes[i] == b'(' && bytes[i + 1] == b'*' { + depth += 1; + i += 2; + continue; + } + if depth > 0 && i + 1 < bytes.len() && bytes[i] == b'*' && bytes[i + 1] == b')' { + depth -= 1; + i += 2; + continue; + } + if depth == 0 { + out.push(bytes[i] as char); + } + i += 1; + } + out +} + +/// `tok` appears in `s` as a delimited token (so `admittedly` or `Foo.admit` +/// do not match the bare keyword). +fn has_token(s: &str, tok: &str) -> bool { + s.split(|c: char| c.is_whitespace() || "(){};,.".contains(c)) + .any(|w| w == tok) +} + +#[cfg(test)] +mod tests { + use super::*; + use crate::lint::run_lints; + use std::path::PathBuf; + + fn lint_str(body: &str) -> LintReport { + let tmp = tempfile::NamedTempFile::new().unwrap(); + std::fs::write(tmp.path(), body).unwrap(); + let roots: [PathBuf; 0] = []; + let ctx = LintContext { + include_root: tmp.path().parent().unwrap(), + entry_modules: &roots, + }; + let rules: Vec> = vec![Box::new(CoqEscapeHatch)]; + run_lints(tmp.path(), &ctx, &rules).unwrap() + } + + #[test] + fn admitted_is_warned() { + let r = lint_str("Theorem t : True.\nProof.\nAdmitted.\n"); + assert_eq!(r.warns().count(), 1); + assert_eq!(r.diagnostics[0].rule, "escape-hatch"); + assert!(r.diagnostics[0].message.contains("Admitted")); + } + + #[test] + fn axiom_and_admit_tactic_are_warned() { + let r = lint_str( + "Axiom em : forall P : Prop, P \\/ ~P.\nTheorem t : True. Proof. admit. Defined.\n", + ); + assert_eq!(r.warns().count(), 2); + } + + #[test] + fn escape_token_in_comment_is_ignored() { + let r = lint_str("Definition x := 0. (* no Admitted here *)\n"); + assert!(r.diagnostics.is_empty()); + let r2 = lint_str("(* Axiom foo : bar. *)\n"); + assert!(r2.diagnostics.is_empty()); + } + + #[test] + fn clean_coq_file_is_silent() { + let r = lint_str("Theorem t : True.\nProof.\nexact I.\nQed.\n"); + assert!(r.diagnostics.is_empty()); + } + + #[test] + fn parameter_is_not_flagged_by_the_lint() { + // Parameter is left to the backend's Section-aware classifier. + let r = lint_str("Parameter State : Type.\n"); + assert!(r.diagnostics.is_empty()); + } +} diff --git a/src/lint/mod.rs b/src/lint/mod.rs index 7f8390f..df6346b 100644 --- a/src/lint/mod.rs +++ b/src/lint/mod.rs @@ -5,6 +5,7 @@ use crate::diagnostic::LintReport; use anyhow::Result; use std::path::{Path, PathBuf}; +pub mod coq; pub mod escape_hatch; pub mod idris2; pub mod lean; diff --git a/src/main.rs b/src/main.rs index dd9daa4..71c3c92 100644 --- a/src/main.rs +++ b/src/main.rs @@ -5,8 +5,8 @@ use anyhow::{Context, Result}; use arghda_core::lint::LintContext; use arghda_core::{ build_dag, build_reason, event, groove_manifest, run_lints, unused, watcher, Agda, AgdaCubical, - Backend, BackendKind, Dispatch, Idris2, Lean, LintRule, Probe, RuleConfig, Smt, State, Verdict, - Workspace, + Backend, BackendKind, Coq, Dispatch, Idris2, Lean, LintRule, Probe, RuleConfig, Smt, State, + Verdict, Workspace, }; use clap::{Parser, Subcommand}; use std::path::{Path, PathBuf}; @@ -17,7 +17,15 @@ use walkdir::WalkDir; type RuleSet = Vec>; /// Every backend `--backend` accepts and `doctor` probes. -const KNOWN_BACKENDS: &[&str] = &["agda", "agda-cubical", "idris2", "lean4", "z3", "cvc5"]; +const KNOWN_BACKENDS: &[&str] = &[ + "agda", + "agda-cubical", + "idris2", + "lean4", + "coq", + "z3", + "cvc5", +]; /// Resolve a `--backend` name to a backend instance. Agda is the default and /// v0.1 reference; Idris2 is the estate ABI language. @@ -27,10 +35,11 @@ fn backend_for(name: &str) -> Result> { "agda-cubical" => Ok(Box::new(AgdaCubical)), "idris2" => Ok(Box::new(Idris2)), "lean4" => Ok(Box::new(Lean)), + "coq" => Ok(Box::new(Coq)), "z3" => Ok(Box::new(Smt::z3())), "cvc5" => Ok(Box::new(Smt::cvc5())), other => anyhow::bail!( - "unknown backend `{other}` (known: agda, agda-cubical, idris2, lean4, z3, cvc5)" + "unknown backend `{other}` (known: agda, agda-cubical, idris2, lean4, coq, z3, cvc5)" ), } } @@ -39,7 +48,7 @@ fn backend_for(name: &str) -> Result> { #[command( name = "arghda", version, - about = "Proof-workspace manager for provers/solvers (Agda, Cubical, Idris2, Lean4, Z3, CVC5)" + about = "Proof-workspace manager for provers/solvers (Agda, Cubical, Idris2, Lean4, Coq, Z3, CVC5)" )] struct Cli { #[command(subcommand)] @@ -67,7 +76,7 @@ enum Cmd { #[arg(long)] config: Option, /// Backend: `agda` (default), `agda-cubical`, `idris2`, `lean4`, - /// `z3`, `cvc5`. + /// `coq`, `z3`, `cvc5`. #[arg(long, default_value = "agda")] backend: String, /// Also run the external `agda-unused` analyser and re-emit its @@ -87,7 +96,7 @@ enum Cmd { #[arg(long)] include_root: Option, /// Backend: `agda` (default), `agda-cubical`, `idris2`, `lean4`, - /// `z3`, `cvc5`. + /// `coq`, `z3`, `cvc5`. #[arg(long, default_value = "agda")] backend: String, /// Where the check runs: `local` (default) or `echidna[=]` @@ -115,7 +124,7 @@ enum Cmd { #[arg(long)] config: Option, /// Backend: `agda` (default), `agda-cubical`, `idris2`, `lean4`, - /// `z3`, `cvc5`. + /// `coq`, `z3`, `cvc5`. #[arg(long, default_value = "agda")] backend: String, }, @@ -139,7 +148,7 @@ enum Cmd { #[arg(long)] config: Option, /// Backend: `agda` (default), `agda-cubical`, `idris2`, `lean4`, - /// `z3`, `cvc5`. + /// `coq`, `z3`, `cvc5`. #[arg(long, default_value = "agda")] backend: String, /// Run the backend on every node to populate REAL prover verdicts diff --git a/src/prover/mod.rs b/src/prover/mod.rs index 04a06e1..7d2c4cf 100644 --- a/src/prover/mod.rs +++ b/src/prover/mod.rs @@ -30,11 +30,13 @@ use std::process::Command; pub mod agda; pub mod idris2; pub mod lean; +pub mod rocq; pub mod smt; pub use agda::{Agda, AgdaCubical}; pub use idris2::Idris2; pub use lean::Lean; +pub use rocq::Coq; pub use smt::Smt; /// The two backend interaction models. diff --git a/src/prover/rocq.rs b/src/prover/rocq.rs new file mode 100644 index 0000000..c3aaa1a --- /dev/null +++ b/src/prover/rocq.rs @@ -0,0 +1,545 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) + +//! The Coq / Rocq backend. +//! +//! Assistant model, with the same soundness subtlety Lean forces on us: a +//! green `coqc` exit does NOT by itself mean "proven". `coqc` compiles a file +//! that closes proofs with `Admitted.` (which turns the goal into an axiom) or +//! 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). +//! * 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`]. +//! * exit 0, otherwise → [`Verdict::Proven`]: `coqc` kernel-checks every `Qed` +//! at compile time, so a clean compile with no escape hatch *is* a checked +//! proof (stronger than Lean, where a bare elaboration needs a `#print +//! axioms` audit). +//! * binary absent → [`Verdict::Unavailable`]. +//! +//! "Genuine unverified postulate" is decided by a Section-aware classifier +//! ([`count_genuine_postulates`]) ported from panic-attack's +//! `count_rocq_unverified_postulates`: `Variable`/`Hypothesis`/`Parameter` +//! inside a `Section … End` are discharged at `End` (not counted), and +//! module-level `Parameter` declarations whose stated type is a carrier +//! (`Type`/`Set`), a decidability witness, or a non-`Prop` function symbol are +//! abstractions awaiting instantiation (not counted). Everything else — +//! notably `Prop`-valued `Axiom`/`Parameter` — is a real postulate. +//! +//! Coq logical names are dotted and map to paths like every other assistant +//! (`Foo.Bar` ↔ `Foo/Bar.v`), so [`crate::graph::module_name_of`] is reused. +//! 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. + +use super::{Backend, BackendKind, Outcome, Verdict}; +use crate::graph; +use crate::lint::{coq::CoqEscapeHatch, LintRule, RuleConfig}; +use anyhow::{Context, Result}; +use std::fs; +use std::path::{Path, PathBuf}; +use std::process::Command; +use std::time::{SystemTime, UNIX_EPOCH}; +use walkdir::WalkDir; + +const TAIL_LINES: usize = 40; + +/// The Coq / Rocq proof assistant. +#[derive(Clone, Copy, Debug, Default)] +pub struct Coq; + +impl Backend for Coq { + fn name(&self) -> &'static str { + "coq" + } + + fn kind(&self) -> BackendKind { + BackendKind::Assistant + } + + fn extensions(&self) -> &'static [&'static str] { + &["v"] + } + + fn safe_mode(&self) -> Option<&'static str> { + // Coq has no global safe flag; soundness is the absence of + // Admitted/admit and of genuine Axiom/Parameter postulates (the + // runtime analogue is `Print Assumptions`). + Some("Print Assumptions") + } + + 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. + let nanos = SystemTime::now() + .duration_since(UNIX_EPOCH) + .map(|d| d.as_nanos()) + .unwrap_or(0); + let out_dir = + 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); + + 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, + exit_code: out.status.code(), + ok: verdict == Verdict::Proven, + output_tail: tail(&combined, TAIL_LINES), + kind: BackendKind::Assistant, + verdict, + }) + } + Err(e) if e.kind() == std::io::ErrorKind::NotFound => { + Ok(Outcome::unavailable(BackendKind::Assistant)) + } + Err(e) => Err(e.into()), + } + } + + fn module_name_of(&self, file: &Path, include_root: &Path) -> Option { + graph::module_name_of(file, include_root) + } + + 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 + } + + fn direct_imports(&self, file: &Path) -> Result> { + let contents = + fs::read_to_string(file).with_context(|| format!("reading {}", file.display()))?; + Ok(parse_requires(&contents)) + } + + fn discover_roots(&self, include_root: &Path) -> Vec { + // Coq has no universal entry-module convention; the estate aggregator + // convention is `All.v` (mirroring Agda's `All.agda`). `_CoqProject`- + // declared file sets are a documented follow-on. + let mut roots = Vec::new(); + for entry in WalkDir::new(include_root) + .into_iter() + .filter_map(|e| e.ok()) + { + let path = entry.path(); + if path.extension().and_then(|s| s.to_str()) != Some("v") { + continue; + } + if path.file_name().and_then(|s| s.to_str()) == Some("All.v") { + roots.push(path.to_path_buf()); + } + } + roots.sort(); + roots + } + + fn lint_rules(&self, _cfg: &RuleConfig) -> Result>> { + Ok(vec![Box::new(CoqEscapeHatch)]) + } + + fn command(&self) -> &'static str { + "coqc" + } +} + +/// 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 ⇒ +/// `Postulated`. A non-zero exit ⇒ `Error`. Admitted dominates a postulate +/// (an unfinished proof is the more severe hole), mirroring Lean's `sorryAx`. +fn coq_verdict(src: &str, exit_ok: bool) -> Verdict { + if !exit_ok { + return Verdict::Error; + } + if has_admit(src) { + return Verdict::Admitted; + } + if count_genuine_postulates(src) > 0 { + return Verdict::Postulated; + } + Verdict::Proven +} + +/// Whether `src` closes a proof with `Admitted.` or uses the `admit` tactic — +/// scanned as delimited tokens over comment-stripped lines so `admittedly` or +/// a `(* admit *)` comment does not match. +fn has_admit(src: &str) -> bool { + for raw in src.lines() { + let line = strip_line_comments(raw); + let trimmed = line.trim_start(); + if trimmed.is_empty() { + continue; + } + for tok in ["Admitted", "admit"] { + if has_token(&line, tok) { + return true; + } + } + } + false +} + +/// Extract the modules a Coq file depends on via `Require` statements. +/// +/// Handles `Require [Import|Export] M1 M2 ….` and `From P Require [Import| +/// Export] M ….` (the `P.M` form is recorded as the bare `M`, since a flat +/// in-tree layout resolves `M.v`; logical-prefix resolution is a follow-on). +/// A bare `Import`/`Export` (namespace directive, not a dependency) is ignored. +/// Statements are assumed to sit on a single logical line (the common case). +fn parse_requires(contents: &str) -> Vec { + let mut out = Vec::new(); + for raw in contents.lines() { + let line = strip_line_comments(raw); + let tokens: Vec<&str> = line.split_whitespace().collect(); + let Some(req_idx) = tokens.iter().position(|t| *t == "Require") else { + continue; + }; + // `From P Require …` is valid; a `Require` anywhere else on the line + // is still the dependency keyword. Modules follow, after an optional + // `Import`/`Export`. + let mut idx = req_idx + 1; + if matches!(tokens.get(idx), Some(&"Import") | Some(&"Export")) { + idx += 1; + } + for tok in &tokens[idx..] { + // The statement terminator is a lone `.` or a trailing `.` on the + // last module token. + let ends = tok.ends_with('.'); + let cleaned = clean_module(tok); + if !cleaned.is_empty() { + out.push(cleaned); + } + if ends { + break; + } + } + } + out +} + +/// Trim a module token to its dotted identifier: drop a single trailing +/// statement-terminator `.` and any surrounding punctuation, keeping internal +/// dots (`Coq.Lists.List.` → `Coq.Lists.List`). +fn clean_module(tok: &str) -> String { + let t = tok.trim_matches(|c: char| !c.is_alphanumeric() && c != '.' && c != '_'); + t.strip_suffix('.') + .unwrap_or(t) + .trim_matches('.') + .to_string() +} + +/// Count Coq `Axiom`/`Parameter` declarations that are genuine unverified +/// postulates, excluding the two legitimate scaffold shapes (ported from +/// panic-attack's `count_rocq_unverified_postulates`): +/// +/// 1. **Section-scoped declarations** between `Section name` and matching +/// `End name` — discharged at `End`, so not floating assumptions. +/// 2. **Module-level abstraction parameters** whose stated type is a carrier +/// (`Type`/`Set`), a decidability witness, or a non-`Prop` function symbol. +/// +/// Everything else is counted, notably `Prop`-valued `Axiom`/`Parameter`. +/// Conservative: unknown shapes default to counted. +fn count_genuine_postulates(code: &str) -> usize { + let mut section_depth: i32 = 0; + let mut count = 0usize; + let mut pending: Option = None; + + for raw_line in code.lines() { + let stripped = strip_line_comments(raw_line); + let trimmed = stripped.trim_start(); + + if trimmed.starts_with("Section ") { + section_depth += 1; + pending = None; + continue; + } + if trimmed.starts_with("End ") && trimmed.contains('.') && section_depth > 0 { + section_depth -= 1; + pending = None; + continue; + } + if section_depth > 0 { + pending = None; + continue; + } + + // Continuation of a multi-line declaration. + if let Some(mut p) = pending.take() { + p.push(' '); + p.push_str(stripped.trim()); + if p.contains('.') { + if !is_abstraction_parameter(&p) { + count += 1; + } + } else { + pending = Some(p); + } + continue; + } + + let is_decl = trimmed.starts_with("Axiom ") || trimmed.starts_with("Parameter "); + if !is_decl { + continue; + } + if stripped.trim_end().ends_with('.') { + if !is_abstraction_parameter(&stripped) { + count += 1; + } + } else { + pending = Some(stripped.trim().to_string()); + } + } + count +} + +/// Classify a Coq `Axiom`/`Parameter` declaration as an abstraction parameter +/// (carrier type, decidability witness, or non-`Prop` function symbol) rather +/// than a postulate. Conservative: unknown shapes return `false` (counted). +fn is_abstraction_parameter(decl: &str) -> bool { + let Some(colon) = decl.find(':') else { + return false; + }; + let typ = decl[colon + 1..].trim(); + let typ = typ.strip_suffix('.').unwrap_or(typ).trim(); + + // 1. Carrier type. + if typ == "Type" || typ == "Set" { + return true; + } + // 2. Decidability witness `forall …, { _ = _ } + { _ <> _ }`. + if typ.contains('{') + && typ.contains('=') + && typ.contains('}') + && typ.contains('+') + && typ.contains("<>") + { + return true; + } + // 3. Function type with a clearly non-`Prop` codomain. + if typ.contains("->") { + let return_type = typ.rsplit("->").next().unwrap_or("").trim(); + if return_type == "Prop" { + return false; + } + let first_word = return_type.split_whitespace().next().unwrap_or(""); + const CONCRETE_RETURNS: &[&str] = &[ + "Q", "R", "Z", "N", "nat", "bool", "list", "option", "prod", "sum", "unit", "Type", + "Set", + ]; + if CONCRETE_RETURNS.contains(&first_word) { + return true; + } + if let Some(c) = first_word.chars().next() { + if c.is_ascii_lowercase() { + return true; + } + } + } + false +} + +/// Remove Coq `(* … *)` comment spans from a single line. Balanced spans are +/// cut out; an unmatched `(*` truncates the rest of the line (a multi-line +/// comment's interior is a documented limitation). +fn strip_line_comments(line: &str) -> String { + let mut out = String::with_capacity(line.len()); + let bytes = line.as_bytes(); + let mut i = 0; + let mut depth = 0u32; + while i < bytes.len() { + if i + 1 < bytes.len() && bytes[i] == b'(' && bytes[i + 1] == b'*' { + depth += 1; + i += 2; + continue; + } + if depth > 0 && i + 1 < bytes.len() && bytes[i] == b'*' && bytes[i + 1] == b')' { + depth -= 1; + i += 2; + continue; + } + if depth == 0 { + out.push(bytes[i] as char); + } + i += 1; + } + out +} + +fn tail(s: &str, n: usize) -> String { + let lines: Vec<&str> = s.lines().collect(); + let start = lines.len().saturating_sub(n); + lines[start..].join("\n") +} + +/// `tok` appears in `s` as a delimited token (so `admittedly` or a +/// namespaced `Foo.admit` do not match the bare keyword). +fn has_token(s: &str, tok: &str) -> bool { + s.split(|c: char| c.is_whitespace() || "(){};,.".contains(c)) + .any(|w| w == tok) +} + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn coq_backend_identity() { + assert_eq!(Coq.name(), "coq"); + assert_eq!(Coq.kind(), BackendKind::Assistant); + assert_eq!(Coq.extensions(), &["v"]); + assert_eq!(Coq.command(), "coqc"); + } + + #[test] + fn module_to_path_uses_v_extension() { + assert_eq!( + Coq.module_to_path("Coq.Lists.List", Path::new("/r")), + PathBuf::from("/r/Coq/Lists/List.v") + ); + } + + #[test] + fn requires_parsed_import_export_and_from() { + let tmp = tempfile::NamedTempFile::new().unwrap(); + std::fs::write( + tmp.path(), + "Require Import Coq.Lists.List.\n\ + Require Export Helper.\n\ + From Stdlib Require Import Arith.\n\ + Require A B.\n\ + Import Namespace.\n\ + Export Other.\n\ + (* Require Import Commented. *)\n", + ) + .unwrap(); + let imports = Coq.direct_imports(tmp.path()).unwrap(); + assert!(imports.contains(&"Coq.Lists.List".to_string())); + assert!(imports.contains(&"Helper".to_string()), "Require Export"); + assert!(imports.contains(&"Arith".to_string()), "From … Require"); + assert!(imports.contains(&"A".to_string()) && imports.contains(&"B".to_string())); + // Bare Import/Export are namespace directives, not edges. + assert!(!imports.iter().any(|i| i == "Namespace" || i == "Other")); + assert!(!imports.iter().any(|i| i.contains("Commented"))); + } + + #[test] + fn verdict_is_honest_about_admit_axiom_and_clean() { + // Non-zero exit is always Error, whatever the source says. + assert_eq!( + coq_verdict("Theorem t : True. Proof. exact I. Qed.\n", false), + Verdict::Error + ); + // Admitted / admit ⇒ Admitted (amber), and dominates a postulate. + assert_eq!( + coq_verdict("Theorem t : True.\nProof.\nAdmitted.\n", true), + Verdict::Admitted + ); + assert_eq!( + coq_verdict( + "Axiom bad : False.\nTheorem t : True.\nProof.\nadmit.\nDefined.\n", + true + ), + Verdict::Admitted + ); + // A genuine Prop-valued Axiom ⇒ Postulated. + assert_eq!( + coq_verdict("Axiom em : forall P : Prop, P \\/ ~P.\n", true), + Verdict::Postulated + ); + // Clean compile with only kernel-checked proofs ⇒ Proven. + assert_eq!( + coq_verdict("Theorem t : True.\nProof.\nexact I.\nQed.\n", true), + Verdict::Proven + ); + } + + #[test] + fn section_scoped_declarations_are_discharged() { + let code = "\ +Section OrderedField.\n\ + Variable R : Type.\n\ + Hypothesis Rplus_comm : forall x y : R, x = y.\n\ + Parameter Rabs : R -> R.\n\ +End OrderedField.\n"; + assert_eq!( + count_genuine_postulates(code), + 0, + "Section-scoped Variable/Hypothesis/Parameter discharge at End" + ); + } + + #[test] + fn module_level_abstractions_are_not_postulates() { + assert_eq!(count_genuine_postulates("Parameter State : Type.\n"), 0); + assert_eq!( + count_genuine_postulates("Parameter dec : forall x y : State, {x = y} + {x <> y}.\n"), + 0 + ); + assert_eq!( + count_genuine_postulates("Parameter kernel : State -> State -> Q.\n"), + 0 + ); + } + + #[test] + fn prop_valued_axioms_are_counted() { + assert_eq!( + count_genuine_postulates("Axiom excluded_middle : forall P : Prop, P \\/ ~P.\n"), + 1 + ); + // Bare `Parameter foo.` with no type is an unknown shape ⇒ counted. + assert_eq!(count_genuine_postulates("Parameter foo.\n"), 1); + } + + #[test] + fn check_file_is_honest_about_availability() { + let tmp = tempfile::tempdir().unwrap(); + let f = tmp.path().join("T.v"); + std::fs::write(&f, "Theorem t : True.\nProof.\nexact I.\nQed.\n").unwrap(); + let out = Coq.check_file(&f, tmp.path()).unwrap(); + if out.available { + assert!(matches!( + out.verdict, + Verdict::Proven | Verdict::Admitted | Verdict::Postulated | Verdict::Error + )); + assert_eq!(out.ok, out.verdict == Verdict::Proven); + } else { + assert_eq!(out.verdict, Verdict::Unavailable); + assert!(!out.ok); + assert!(out.exit_code.is_none()); + } + } +} diff --git a/tests/coq.rs b/tests/coq.rs new file mode 100644 index 0000000..5e5c774 --- /dev/null +++ b/tests/coq.rs @@ -0,0 +1,75 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) + +//! Coq / Rocq backend, exercised through the backend-parametric graph/dag/ +//! reason path. These tests are hermetic — they only parse `.v` text (module +//! names + `Require` edges), so they run with or without the `coqc` binary +//! present. The real compile + verdict classification (`check_file`, +//! Section-aware postulate counting) is covered by the unit tests in +//! `src/prover/rocq.rs` (honest either way) and by manual dogfooding against +//! Coq 8.18.0. + +use arghda_core::lint::unpinned_headline::DEFAULT_HEADLINE_PATTERN; +use arghda_core::{build_dag, build_reason, Backend, Coq, LintRule}; +use std::collections::{BTreeMap, BTreeSet}; +use std::path::PathBuf; + +fn coq_fixture() -> PathBuf { + let mut p = PathBuf::from(env!("CARGO_MANIFEST_DIR")); + p.push("tests"); + p.push("fixtures"); + p.push("coq"); + p +} + +/// The graph path needs no lint rules; a typed empty pack. +fn no_rules() -> Vec> { + Vec::new() +} + +#[test] +fn coq_require_graph_over_the_fixture() { + let root = coq_fixture(); + let roots = Coq.discover_roots(&root); + let dag = build_dag(&root, &roots, &no_rules(), DEFAULT_HEADLINE_PATTERN, &Coq).unwrap(); + + let mut ids: Vec<&str> = dag.nodes.iter().map(|n| n.id.as_str()).collect(); + ids.sort_unstable(); + assert_eq!(ids, vec!["All", "Base", "Orphan", "Util"]); + + // `Require Import Base` / `Require Import Util` become edges. + assert!(dag + .edges + .iter() + .any(|e| e.from == "All" && e.to == "Base" && e.kind == "imports")); + assert!(dag.edges.iter().any(|e| e.from == "All" && e.to == "Util")); + assert!(dag.edges.iter().any(|e| e.from == "Util" && e.to == "Base")); + // Nothing requires Orphan. + assert!(!dag.edges.iter().any(|e| e.to == "Orphan")); +} + +#[test] +fn coq_discover_roots_finds_all_v() { + let root = coq_fixture(); + let roots = Coq.discover_roots(&root); + let names: Vec = roots + .iter() + .map(|p| p.file_name().unwrap().to_str().unwrap().to_string()) + .collect(); + assert_eq!(names, vec!["All.v".to_string()]); +} + +#[test] +fn coq_reason_graph_wires_the_all_cone() { + let root = coq_fixture(); + let roots = Coq.discover_roots(&root); + let dag = build_dag(&root, &roots, &no_rules(), DEFAULT_HEADLINE_PATTERN, &Coq).unwrap(); + let doc = build_reason(dag, &Coq, &BTreeMap::new(), &BTreeSet::new()); + + assert_eq!(doc.crt_roots, vec!["All".to_string()]); + let wired = |id: &str| doc.nodes.iter().find(|n| n.id == id).unwrap().wired; + assert!(wired("All")); + assert!(wired("Util")); + assert!(wired("Base")); + assert!(!wired("Orphan"), "Orphan must be unwired"); +} diff --git a/tests/fixtures/coq/All.v b/tests/fixtures/coq/All.v new file mode 100644 index 0000000..ae4dfb9 --- /dev/null +++ b/tests/fixtures/coq/All.v @@ -0,0 +1,3 @@ +Require Import Base. +Require Import Util. +Definition top : nat := helper. diff --git a/tests/fixtures/coq/Base.v b/tests/fixtures/coq/Base.v new file mode 100644 index 0000000..92cef9a --- /dev/null +++ b/tests/fixtures/coq/Base.v @@ -0,0 +1 @@ +Definition base : nat := 0. diff --git a/tests/fixtures/coq/Orphan.v b/tests/fixtures/coq/Orphan.v new file mode 100644 index 0000000..8d286f9 --- /dev/null +++ b/tests/fixtures/coq/Orphan.v @@ -0,0 +1 @@ +Definition orphan : nat := 1. diff --git a/tests/fixtures/coq/Util.v b/tests/fixtures/coq/Util.v new file mode 100644 index 0000000..8943ef4 --- /dev/null +++ b/tests/fixtures/coq/Util.v @@ -0,0 +1,2 @@ +Require Import Base. +Definition helper : nat := base.