diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index 09f9acc..00c86e4 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -44,7 +44,7 @@ milestones = [ { 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 = 100 }, { name = "M2: Cubical-Agda variant (Agda::cubical(), --cubical --safe island)", completion = 100 }, { name = "M3: Flying-Logic reasoning graph (src/reason: And|Or juncts, demote-only cycle-safe Verdict propagation, additive studio JSON)", completion = 100 }, - { name = "M4: Idris2 adapter (core/ABI language: .ipkg/--check/totality; escape-hatches)", completion = 95 }, + { name = "M4: Idris2 adapter (core/ABI language: .ipkg/--check/totality; escape-hatches)", completion = 100 }, { 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 }, @@ -114,6 +114,22 @@ milestones = [ # --backend idris2` over an ipkg fixture → crt_roots ['App'], App+Helper wired. # M4 now 95% (remaining: totality-hole `?name` + per-def `partial` lint). # +# 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 +# holes `?name` (incomplete terms/proofs). src/lint/idris2.rs: `holes()` finds a +# `?` that begins a token (start / after ws / ([{,;= ) and is followed by an +# identifier — so a hole `?goal` matches but a user operator `` does not; +# `strip_strings()` blanks double-quoted literals (honouring \" ) first so a +# `"?x"` in a string is not a false hole. All under the shared `escape-hatch` +# rule name → the reason graph caps hits at amber. 173 tests (+5 idris2 lint +# unit: per-def partial, hole, hole-in-string ignored, `` not a hole, `total` +# not flagged). DOGFOODED vs real idris2 0.7.0: a file with `partial loop` + +# `f = ?rhs` — `idris2 --check --source-dir` exits 0 (the silent-failure class); +# `arghda scan --backend idris2` flags both (partial + ?rhs); `reason --check +# --backend idris2` → Holey self=admitted, effective=admitted, evidence +# "prover: proven; escape-hatch → admitted" (green exit correctly capped amber). +# # M6 FOLLOW-ON landed 2026-07-01 (M6 → 100%): lake-env import resolution — the # Lean audit now reaches IMPORTED files, not just import-free ones. When a # `lakefile.lean`/`lakefile.toml` is found at/above the file (`lake_root`), both @@ -392,12 +408,12 @@ actions = [ "ENGINE-SPINE DELIVERABLE COMPLETE: M0-M7 + M11 all landed. v0.1 spec closed. Six backends (agda, agda-cubical, idris2, lean4 Assistant; z3, cvc5 Solver) + reasoning graph + doctor + groove + dispatch seam. Remaining work is refinement + the heavy tail:", "M7 follow-on: the real Echidna orchestrator HTTP client (feature-gated), once Echidna's API is confirmed — only Dispatch::run changes.", "M6 follow-on: DONE (M6 → 100%) — lake-env resolution (`lake env lean` under a lakefile) so IMPORTED Lean files elaborate + get #print-axioms-audited too, not just import-free ones. Dogfooded on a built lake project.", - "M4 follow-on: .ipkg-declared roots DONE; remaining = totality-hole (?name) + per-def `partial` lint.", + "M4 follow-on: DONE (M4 → 100%) — totality-hole (?name) + per-def `partial` lint added to the Idris2 escape-hatch rule; dogfooded vs real idris2 0.7.0 (green --check exit correctly capped to amber).", "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 (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 (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.", - "Next, climb up: M4 (totality-hole ?name + per-def partial lint for Idris2), M7 (real Echidna HTTP client, feature-gated — but FIRST confirm Echidna's API actually exists; if not, keep the honest stub). Each its own focused draft PR, gate green, real-tool dogfood where installed.", + "Only M7 remains: the real Echidna HTTP client (feature-gated) — but FIRST confirm Echidna's API actually exists (search estate/GitHub for an echidna repo with a documented HTTP API); if it does not, keep the honest Unavailable stub and say so plainly rather than invent a contract. After M7 the roadmap's tractable items are exhausted.", ] [maintenance-status] @@ -406,9 +422,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-M6-followon: 125 lib + 43 integration = 168 tests pass. 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 +# 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). +# 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 # (proven/error via accom+verifier+.err; MIZFILES=/opt/mizar; doctor [OK] # mizar). M9 Isabelle dogfooded vs Isabelle2025; M8 Coq dogfooded vs coqc diff --git a/src/lint/idris2.rs b/src/lint/idris2.rs index 36fb28c..e3713d6 100644 --- a/src/lint/idris2.rs +++ b/src/lint/idris2.rs @@ -9,11 +9,12 @@ //! in Idris2 and a `believe_me` in Agda get the same honest treatment. //! //! Flags the Idris2 trust/escape primitives `believe_me`, `assert_total`, -//! `assert_smaller`, `idris_crash`, and the `%default partial` directive. -//! Idris2 `--check` exits 0 even when these are present, so without this rule -//! they would silently ride along in an otherwise-green verdict — exactly the -//! silent-failure class arghda exists to surface. Totality holes (`?name`) -//! and per-def `partial` modifiers are a documented follow-on. +//! `assert_smaller`, `idris_crash`, the `%default partial` directive, a +//! per-definition `partial` modifier (opts that definition out of totality +//! checking), and totality holes `?name` (incomplete terms/proofs). Idris2 +//! `--check` exits 0 even when these are present, so without this rule they +//! would silently ride along in an otherwise-green verdict — exactly the +//! silent-failure class arghda exists to surface. use super::{LintContext, LintRule}; use crate::diagnostic::{Diagnostic, LintReport, Severity}; @@ -45,7 +46,10 @@ impl LintRule for Idris2EscapeHatch { if trimmed.starts_with("--") { continue; // whole-line comment } - // The `%default partial` directive turns off totality checking. + // Everything below ignores a trailing line comment. + let code = line.split(" --").next().unwrap_or(line); + // The `%default partial` directive turns off totality checking + // file-wide. if trimmed.starts_with("%default") && trimmed.contains("partial") { report.push(warn( self.name(), @@ -53,9 +57,18 @@ impl LintRule for Idris2EscapeHatch { i + 1, "totality escape directive `%default partial`".to_string(), )); + } else if has_token(code, "partial") { + // A per-definition `partial` modifier opts that definition out + // of totality checking (distinct from the file-wide directive + // above, which is already reported). + report.push(warn( + self.name(), + file, + i + 1, + "totality opt-out `partial` modifier".to_string(), + )); } - // Trust/escape primitives, ignoring any trailing line comment. - let code = line.split(" --").next().unwrap_or(line); + // Trust/escape primitives. for tok in ESCAPE_TOKENS { if has_token(code, tok) { report.push(warn( @@ -66,11 +79,80 @@ impl LintRule for Idris2EscapeHatch { )); } } + // Totality holes `?name` — incomplete terms/proofs that `--check` + // defers rather than rejects. String literals are blanked first so + // a `"?x"` inside a string does not match. + for hole in holes(&strip_strings(code)) { + report.push(warn( + self.name(), + file, + i + 1, + format!("totality hole `?{hole}`"), + )); + } } Ok(()) } } +/// Blank out double-quoted string literals (content → spaces), honouring `\"` +/// escapes, so a `?name` inside a string is not mistaken for a hole. +fn strip_strings(line: &str) -> String { + let mut out = String::with_capacity(line.len()); + let mut in_str = false; + let mut escaped = false; + for c in line.chars() { + if in_str { + if escaped { + escaped = false; + } else if c == '\\' { + escaped = true; + } else if c == '"' { + in_str = false; + } + out.push(' '); + } else if c == '"' { + in_str = true; + out.push(' '); + } else { + out.push(c); + } + } + out +} + +/// The hole names in `code`: a `?` that begins a token (start of line or after +/// whitespace / an opening bracket / a separator / `=`) and is followed by an +/// identifier. This distinguishes a hole `?goal` from a user operator like +/// `` (where `?` is surrounded by symbol chars). +fn holes(code: &str) -> Vec { + let b = code.as_bytes(); + let mut out = Vec::new(); + let mut i = 0; + while i < b.len() { + if b[i] == b'?' { + let prev_ok = i == 0 + || matches!( + b[i - 1], + b' ' | b'\t' | b'(' | b'[' | b'{' | b',' | b';' | b'=' + ); + let next_ok = i + 1 < b.len() && (b[i + 1].is_ascii_alphabetic() || b[i + 1] == b'_'); + if prev_ok && next_ok { + let mut j = i + 1; + while j < b.len() && (b[j].is_ascii_alphanumeric() || b[j] == b'_' || b[j] == b'\'') + { + j += 1; + } + out.push(code[i + 1..j].to_string()); + i = j; + continue; + } + } + i += 1; + } + out +} + fn warn(rule: &str, file: &Path, line: usize, message: String) -> Diagnostic { Diagnostic { rule: rule.to_string(), @@ -137,4 +219,38 @@ mod tests { let r = lint_str("module M\n\ngreeting : String\ngreeting = \"hi\"\n"); assert!(r.diagnostics.is_empty()); } + + #[test] + fn per_def_partial_modifier_is_warned() { + let r = lint_str("module M\n\npartial\nloop : Nat -> Nat\nloop x = loop x\n"); + assert_eq!(r.warns().count(), 1); + assert!(r.diagnostics[0].message.contains("partial")); + } + + #[test] + fn totality_hole_is_warned() { + let r = lint_str("module M\n\nf : Nat\nf = ?rhs\n"); + assert_eq!(r.warns().count(), 1); + assert_eq!(r.diagnostics[0].rule, "escape-hatch"); + assert!(r.diagnostics[0].message.contains("?rhs")); + } + + #[test] + fn hole_inside_a_string_is_not_flagged() { + let r = lint_str("module M\n\nmsg : String\nmsg = \"what is ?this\"\n"); + assert!(r.diagnostics.is_empty()); + } + + #[test] + fn question_operator_is_not_a_hole() { + // A user operator like `` has `?` between symbol chars — not a hole. + let r = lint_str("module M\n\n() : Maybe a -> a -> a\n"); + assert!(r.diagnostics.is_empty()); + } + + #[test] + fn total_modifier_is_not_flagged() { + let r = lint_str("module M\n\ntotal\ng : Nat -> Nat\ng x = x\n"); + assert!(r.diagnostics.is_empty()); + } }