From 9764a2906777a2c149250aa0c9157db597fcd123 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 27 Oct 2026 03:37:37 +0000 Subject: [PATCH 01/16] fix(corpus): canonicaliser no longer panics on an unbalanced trailing bracket `matching` returns the last index when a bracket is unbalanced. For an opening bracket that is itself the last token that is the bracket's own index, and all eight `open + 1..close` slices in canonical.rs then panic ("slice index starts at 1 but ends at 0"). Real corpus statements that are truncated mid-term reach this through `structural_key`, which both `corpus ingest` and the octad identity keys call. A `between` helper takes the interior with `get`, so the interior is empty instead of a panic. Balanced input takes exactly the same path as before: no key changes and no scheme bump. Reproduced first: the new `unbalanced_trailing_bracket_does_not_panic` test panics on the old code at `unwrap_assert` and passes now; the existing canonical tests still pass unchanged. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01WS4mfQeC3N1DWjcCQJaQqw --- src/rust/corpus/canonical.rs | 57 +++++++++++++++++++++++++++++++----- 1 file changed, 49 insertions(+), 8 deletions(-) diff --git a/src/rust/corpus/canonical.rs b/src/rust/corpus/canonical.rs index d3558b5d..0c5790cb 100644 --- a/src/rust/corpus/canonical.rs +++ b/src/rust/corpus/canonical.rs @@ -418,6 +418,14 @@ fn matching(toks: &[Tk], at: usize) -> usize { toks.len().saturating_sub(1) } +/// The tokens strictly between an opening bracket at `open` and the index +/// [`matching`] returned for it. Empty when nothing lies between, which +/// includes an unbalanced opening bracket that is the last token: there +/// [`matching`] returns `open` itself, and slicing `open + 1..open` panics. +fn between(toks: &[Tk], open: usize, close: usize) -> &[Tk] { + toks.get(open + 1..close).unwrap_or(&[]) +} + /// Agda writes operators as names: `_<_`, `_+_`, `_≡_`. Read the wrapped /// symbol as one atom so it is not mistaken for three punctuation tokens. fn glue_agda_operators(toks: &[Tk]) -> Vec { @@ -495,7 +503,7 @@ fn unwrap_assert(toks: Vec) -> Vec { if j + 1 != cur.len() { return cur; } - let inner = cur[1..j].to_vec(); + let inner = between(&cur, 0, j).to_vec(); let head_is_assert = match inner.first() { Some(Tk::Id(s)) => matches!( s.to_lowercase().as_str(), @@ -609,7 +617,7 @@ fn extract_binders(toks: &[Tk]) -> (Vec, Binders) { // 1. leading binder group without a keyword while cur.first().map(is_open).unwrap_or(false) { let j = matching(&cur, 0); - let (names, sort) = split_binder_group(&cur[1..j]); + let (names, sort) = split_binder_group(between(&cur, 0, j)); if names.is_empty() { break; } @@ -620,7 +628,7 @@ fn extract_binders(toks: &[Tk]) -> (Vec, Binders) { if !after_ok { break; } - if !has_colon(&cur[1..j]) { + if !has_colon(between(&cur, 0, j)) { break; } for n in &names { @@ -633,20 +641,20 @@ fn extract_binders(toks: &[Tk]) -> (Vec, Binders) { if cur.first().map(is_open).unwrap_or(false) { let j = matching(&cur, 0); if j + 1 == cur.len() { - let inner: Vec = cur[1..j].to_vec(); + let inner: Vec = between(&cur, 0, j).to_vec(); let head_ok = matches!(inner.first(), Some(Tk::Id(s)) if is_pi_kw(s) || is_lam_kw(s)); if head_ok { let rest: Vec = inner[1..].to_vec(); if rest.first().map(is_open).unwrap_or(false) { let m = matching(&rest, 0); - let group: Vec = rest[1..m].to_vec(); + let group: Vec = between(&rest, 0, m).to_vec(); let mut names: Vec = Vec::new(); let mut sorts: Vec = Vec::new(); if group.first().map(is_open).unwrap_or(false) { let mut k = 0usize; while k < group.len() && is_open(&group[k]) { let e = matching(&group, k); - let (n, s) = split_binder_group(&group[k + 1..e]); + let (n, s) = split_binder_group(between(&group, k, e)); for name in n { names.push(name); sorts.push(s.clone()); @@ -701,7 +709,7 @@ fn extract_binders(toks: &[Tk]) -> (Vec, Binders) { } if is_open(&cur[i]) { let m = matching(&cur, i); - let (n, s) = split_binder_group(&cur[i + 1..m]); + let (n, s) = split_binder_group(between(&cur, i, m)); if n.is_empty() { break; } @@ -763,7 +771,7 @@ fn drop_ascriptions(toks: &[Tk]) -> Vec { while i < toks.len() { if is_open(&toks[i]) { let j = matching(toks, i); - let inner: Vec = toks[i + 1..j].to_vec(); + let inner: Vec = between(toks, i, j).to_vec(); let ids: Vec<&String> = inner .iter() .filter_map(|t| match t { @@ -1279,4 +1287,37 @@ mod tests { assert!(toks.contains(&"v0".to_string())); assert!(!toks.iter().any(|t| t.contains("forall"))); } + + /// An opening bracket with nothing after it used to make `matching` + /// return the bracket's own index, and every `open + 1..close` slice + /// then panicked. Corpus statements truncated mid-term hit this. + #[test] + fn unbalanced_trailing_bracket_does_not_panic() { + for s in [ + "(", + "f x = (", + "forall (", + "∀ x, x = (", + "(assert (", + "(forall ((x Nat)) (", + "theorem t (x : nat) : x = (", + ] { + let k = structural_key(s); + assert_eq!(k.key.len(), 64, "{s:?}"); + assert_eq!(k.scheme, SCHEME); + } + } + + /// The guard is a no-op on balanced input: keys stay as they were. + #[test] + fn balanced_input_keys_are_unchanged_by_the_bracket_guard() { + assert_eq!( + canonical_shape("forall x y : nat, x + y = y + x"), + "(PI [NAT NAT] (EQ (ADD v0 v1) (ADD v1 v0)))" + ); + assert_eq!( + canonical_shape("(assert (forall ((x Nat) (y Nat)) (= (+ x y) (+ y x))))"), + "(PI [NAT NAT] (EQ (ADD v0 v1) (ADD v1 v0)))" + ); + } } From 7f80363da4ebd9749af481a1d1ea14dfd3e51950 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 27 Oct 2026 04:22:15 +0000 Subject: [PATCH 02/16] feat(corpus): StructuralKey::complete says whether a key covers the statement MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit When dk-shape-v1 cannot read a statement it rarely falls back to its text tier: it returns a structural-tier key for the prefix it did read, and different statements share that prefix. Measured on training_data/ (see the lexicon-v2 ADR, PR 3 results) this is most of several corpora. `complete` is false when the parser stops early, when the body holds notation the scheme has no rule for (HOL `!` `?` `@` `\` binders, Isabelle `\<…>` escapes, Lean 3 `$`), when the header drop discards a statement's own leading tokens (a header-less `exp(0) = 1` keys as `(EQ 0 1)`, shared with `cos(0) = 1`), when a declaration keyword is dropped with no declaration after it (`FACT 1 = 1` keys as `1 = 1`), or when a leading bracket group is misread as a binder telescope (`(forall x : nat, P x) -> Q` keys as `(PI [NAT NAT] v0)`). No key changes: the flag qualifies the key, and every fixture spelling still parses completely. Fixing the rules themselves changes keys and is left for a dk-shape-v2 decision (D6). Tests pin each flagged behaviour and that the existing keys are unchanged. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01WS4mfQeC3N1DWjcCQJaQqw --- docs/CORPUS.adoc | 12 ++ ...0-22-structural-cross-prover-identity.adoc | 7 + src/rust/corpus/canonical.rs | 187 ++++++++++++++++-- 3 files changed, 193 insertions(+), 13 deletions(-) diff --git a/docs/CORPUS.adoc b/docs/CORPUS.adoc index 13d44e02..52b25b40 100644 --- a/docs/CORPUS.adoc +++ b/docs/CORPUS.adoc @@ -242,6 +242,18 @@ Isabelle writes the same fact without binders and Why3 states it over therefore *tiered*: exact structural key first, skeleton key second. Any consumer that only compares one field should compare both. +A key is only as good as the parse behind it. `+StructuralKey::complete+` +says whether the canonicaliser read the *whole* statement; when it did not +(its parser stopped early, it met notation it has no rule for — HOL's `+!+` +and `+?+` binders, Isabelle's `+\<…>+` escapes — or a header drop discarded +the statement's own leading tokens), the key is still reported at the +structural tier but is a *prefix* that other statements share. Treat an +incomplete key as no identity at all. Measured on `+training_data/+`, the +share of statements read completely ranges from under 1% (Isabelle/ZF) to +over 90% (λProlog); see +`+docs/decisions/2026-10-19-lexicon-v2-and-identity-arbitration.adoc+` +(PR 3 results) and `+echidna lexicon scan+`. + The CLI surfaces it directly: [source,bash] diff --git a/docs/decisions/2026-10-22-structural-cross-prover-identity.adoc b/docs/decisions/2026-10-22-structural-cross-prover-identity.adoc index 1fdc31b5..8475faac 100644 --- a/docs/decisions/2026-10-22-structural-cross-prover-identity.adoc +++ b/docs/decisions/2026-10-22-structural-cross-prover-identity.adoc @@ -146,6 +146,13 @@ legacy name-tail hashes differ. estate's corpora; it is not a grammar for any prover. Statements it cannot parse fall back to a whitespace-normalised text key at tier 3 (`+KeyTier::Text+`), which is honest but weak — worth measuring. + *Measured 2026-10-27* (`+echidna lexicon scan+` over thirteen + `+training_data/+` corpora): statements it cannot *fully* read mostly do + not fall back to tier 3; they get a structural-tier key for the prefix it + did read, which distinct statements share. `+StructuralKey::complete+` + now reports that, without changing any key, and four rule-level causes + of false identity are recorded for a `+dk-shape-v2+` decision in + `+2026-10-19-lexicon-v2-and-identity-arbitration.adoc+` (PR 3 results). * Sorts are compared by name. `+Nat+` in Lean and `+nat+` in Coq agree because both are aliased to `+NAT+`; type classes and universe levels are not modelled. diff --git a/src/rust/corpus/canonical.rs b/src/rust/corpus/canonical.rs index 0c5790cb..0f8e8ba8 100644 --- a/src/rust/corpus/canonical.rs +++ b/src/rust/corpus/canonical.rs @@ -128,6 +128,18 @@ pub struct StructuralKey { pub skeleton_key: String, /// Which tier this declaration's shape is trustworthy at. pub tier: KeyTier, + /// Whether the shape accounts for the whole statement. False when the + /// parser stopped early (anything but a trailing `.`/`,`/`;` or an + /// unmatched closing bracket left over), when the body holds notation + /// this scheme has no rule for ([`is_unread_notation`]), when the header + /// drop discarded tokens that were not a declared head, or when a leading + /// bracket group was misread as a binder telescope. In each case the + /// shape is still reported at the structural tier but stands for part of + /// the statement, and different statements can share it. Always `false` + /// at the text tier. Not part of `key`: it qualifies the key, so adding + /// it changed no key. + #[serde(default)] + pub complete: bool, } // =========================================================================== @@ -463,15 +475,37 @@ fn has_colon(toks: &[Tk]) -> bool { .any(|t| matches!(t, Tk::Sym(s) if s == ":" || s == "::")) } +/// Whether a top-level `:` occurs anywhere in `toks` (depth 0 relative to +/// the start of the slice). +fn colon_at_top(toks: &[Tk]) -> bool { + let mut depth = 0usize; + for t in toks { + if is_open(t) { + depth += 1; + } else if is_close(t) { + depth = depth.saturating_sub(1); + } else if depth == 0 && matches!(t, Tk::Sym(s) if s == ":" || s == "::=") { + return true; + } + } + false +} + /// `+-comm : body` and `addComm : body` and `: Π …` all have the declared /// name before a top-level colon; drop it. A group that starts the /// statement (`(x y : Nat) : body`) means there is no head to drop. -fn drop_declared_head(toks: Vec) -> Vec { +/// +/// The second value reports a drop that was *not* a declared head: the +/// first top-level bracket comes after other tokens and no top-level colon +/// follows it, so the dropped tokens were the statement's own (`f (g x) = y` +/// loses `f`). The key is unchanged; [`StructuralKey::complete`] reports it. +fn drop_declared_head(toks: Vec) -> (Vec, bool) { let mut depth = 0usize; for (i, t) in toks.iter().enumerate() { if is_open(t) { if depth == 0 { - return toks[i..].to_vec(); + let unexplained = i > 0 && !colon_at_top(&toks[i..]); + return (toks[i..].to_vec(), unexplained); } depth += 1; } else if is_close(t) { @@ -479,17 +513,17 @@ fn drop_declared_head(toks: Vec) -> Vec { } else if depth == 0 { if let Tk::Sym(s) = t { if s == ":" || s == "::=" { - return toks[i + 1..].to_vec(); + return (toks[i + 1..].to_vec(), false); } } if let Tk::Id(s) = t { if is_pi_kw(s) || is_lam_kw(s) { - return toks[i..].to_vec(); + return (toks[i..].to_vec(), false); } } } } - toks + (toks, false) } /// `(assert (forall …))` → `(forall …)`. @@ -518,14 +552,22 @@ fn unwrap_assert(toks: Vec) -> Vec { } } -fn strip_header(toks: &[Tk]) -> Vec { +/// The statement body with any declaration header and proof body removed, and +/// whether the header drop discarded tokens that were not a declared head: +/// a bracket drop (see [`drop_declared_head`]), or a declaration keyword +/// with no top-level `:` after it. Keywords match case-insensitively, so a +/// statement that merely *starts* with one (HOL4's `FACT 1 = 1`, keyed as +/// `1 = 1`) loses it; without a following colon nothing was declared. +fn strip_header(toks: &[Tk]) -> (Vec, bool) { let mut cur = unwrap_assert(glue_agda_operators(toks)); // declaration keyword + declared name + let mut dropped_kw = false; loop { let drops_kw = matches!(cur.first(), Some(Tk::Id(s)) if is_decl_kw(s)); if !drops_kw { break; } + dropped_kw = true; cur.remove(0); if matches!(cur.first(), Some(Tk::Id(_))) { cur.remove(0); @@ -551,7 +593,9 @@ fn strip_header(toks: &[Tk]) -> Vec { Some(i) => cur[..i].to_vec(), None => cur, }; - drop_declared_head(cur) + let keyword_unexplained = dropped_kw && !colon_at_top(&cur); + let (body, head_unexplained) = drop_declared_head(cur); + (body, head_unexplained || keyword_unexplained) } /// `x y : Nat` → (["x","y"], NAT); SMT-LIB `x Nat` likewise. @@ -592,6 +636,11 @@ fn sort_name(toks: &[Tk]) -> String { struct Binders { names: Vec, sorts: Vec, + /// A leading bracket group was read as a telescope although one of its + /// "names" is a binder keyword: `(forall x : nat, P x) -> Q` binds + /// `forall` and `x` and keeps only `Q`. Reported through + /// [`StructuralKey::complete`]; the key is unchanged. + misread: bool, } impl Binders { @@ -631,6 +680,9 @@ fn extract_binders(toks: &[Tk]) -> (Vec, Binders) { if !has_colon(between(&cur, 0, j)) { break; } + if names.iter().any(|n| is_pi_kw(n) || is_lam_kw(n)) { + bound.misread = true; + } for n in &names { bound.push(std::slice::from_ref(n), &sort); } @@ -828,6 +880,18 @@ impl Parser { self.toks.get(self.i) } + /// Whether everything after the cursor is ignorable: a statement + /// terminator (`.`, `,`, `;`) or an unmatched closing bracket. + fn rest_is_ignorable(&self) -> bool { + self.toks[self.i.min(self.toks.len())..] + .iter() + .all(|t| match t { + Tk::Close(_) => true, + Tk::Sym(s) => matches!(s.as_str(), "." | "," | ";"), + _ => false, + }) + } + /// Canonical operator starting at the cursor, if any. fn op_at(&self) -> Option<&'static str> { match self.peek()? { @@ -1077,13 +1141,30 @@ fn number_variables(body: &[Tk], bound: &Binders) -> std::collections::HashMap (String, String) { - let toks = strip_header(&lex(statement)); +/// Tokens that introduce notation this scheme has no rule for: HOL's `!`, +/// `?`, `@` and `\` binders, Isabelle's `\<…>` symbol escapes (which lex as +/// `\`, `<`, name, `>`), and Lean 3's `$` application. The parser reads them +/// as plain names and consumes them, so a shape can look complete and still +/// be wrong; their presence marks the key incomplete. Over-cautious by +/// design: Lean's `s \ t` set difference is flagged too. +fn is_unread_notation(t: &Tk) -> bool { + matches!(t, Tk::Sym(s) if matches!(s.as_str(), "\\" | "!" | "?" | "@" | "$")) +} + +/// Both canonical forms from one pass, and whether the shape accounts for +/// the whole statement: `(shape, skeleton, complete)`. Complete means the +/// header drop discarded only a declared head, no leading group was misread +/// as a telescope, the body holds no unread notation, and the parser +/// consumed the body. +fn normalise(statement: &str) -> (String, String, bool) { + let (toks, dropped_body) = strip_header(&lex(statement)); let toks = drop_ascriptions(&toks); let (body, bound) = extract_binders(&toks); let varmap = number_variables(&body, &bound); - let ast = Parser::new(body, varmap).expr(0); + let unread = body.iter().any(is_unread_notation); + let mut parser = Parser::new(body, varmap); + let ast = parser.expr(0); + let complete = parser.rest_is_ignorable() && !unread && !dropped_body && !bound.misread; let core = render(&ast, false); let skel = render(&ast, true); @@ -1101,7 +1182,7 @@ fn normalise(statement: &str) -> (String, String) { } else { skel }; - (shape, skeleton) + (shape, skeleton, complete) } /// Canonical prefix shape of `statement`, binder prefix included. @@ -1120,7 +1201,7 @@ pub fn canonical_skeleton(statement: &str) -> String { /// binders and sorts erased (covers provers that elide them); and finally /// whitespace-normalised text (covers statements that are not terms). pub fn structural_key(statement: &str) -> StructuralKey { - let (shape, skeleton) = normalise(statement); + let (shape, skeleton, parsed_all) = normalise(statement); let (shape, skeleton, tier) = if !shape.is_empty() { (shape, skeleton, KeyTier::Structural) @@ -1137,6 +1218,7 @@ pub fn structural_key(statement: &str) -> StructuralKey { skeleton_key: sha256_hex(&skeleton), shape, skeleton, + complete: parsed_all && tier != KeyTier::Text, tier, } } @@ -1308,6 +1390,85 @@ mod tests { } } + /// Every fixture spelling parses completely; the flag does not change + /// any key. + #[test] + fn fixture_spellings_parse_completely() { + for (prover, s) in ADD_COMM { + let k = structural_key(s); + assert!(k.complete, "{prover}: {s:?} -> {}", k.shape); + } + assert!(structural_key("Lemma add_comm : forall x y : nat, x + y = y + x.").complete); + } + + /// Statements the scheme cannot read are marked incomplete even though + /// they still get a structural-tier key. + #[test] + fn unread_notation_and_early_stops_are_incomplete() { + for s in [ + // HOL binders + "!m n. m + n = n + m", + "?x. x = 0", + "(\\x. x) = I", + // Isabelle ASCII symbol escapes + "x \\ y \\ f x = f y", + // Lean 3 `$` + "f $ g x = h x", + ] { + let k = structural_key(s); + assert!(!k.complete, "{s:?} -> {} should be incomplete", k.shape); + } + // Text tier is never complete. + assert!(!structural_key("data Bool where true false").complete); + } + + /// A statement with no declared head used to lose everything before its + /// first top-level bracket (`exp(&0) = &1` keyed as `(EQ (& 0) (& 1))`, + /// shared with `cos(&0) = &1`). The key is unchanged here; the drop is + /// reported as incomplete so no consumer treats the prefix as identity. + #[test] + fn header_less_bracket_drop_is_incomplete() { + let exp = structural_key("exp(0) = 1"); + let cos = structural_key("cos(0) = 1"); + assert_eq!(exp.key, cos.key, "the dk-shape-v1 behaviour this flags"); + assert!(!exp.complete && !cos.complete); + assert!(!structural_key("closed (closure M)").complete); + // A real declared head before a group is still a head. + let lean = structural_key("theorem t (x y : nat) : x + y = y + x"); + assert!(lean.complete, "{}", lean.shape); + let idris = structural_key("addComm : (x, y : Nat) -> x + y = y + x"); + assert!(idris.complete, "{}", idris.shape); + } + + /// `FACT` is HOL's factorial and also matches the `fact` keyword: the + /// key drops it (`FACT 1 = 1` keys as `1 = 1`), so the key is reported + /// incomplete. A keyword followed by a declaration is still complete. + #[test] + fn keyword_drop_without_a_declaration_is_incomplete() { + let fact = structural_key("FACT 1 = 1"); + assert_eq!( + fact.key, + structural_key("1 = 1").key, + "the behaviour this flags" + ); + assert!(!fact.complete); + assert!(structural_key("1 = 1").complete); + assert!(structural_key("Lemma add_comm : forall x y : nat, x + y = y + x.").complete); + assert!(structural_key("theorem t (x y : nat) : x + y = y + x").complete); + } + + /// A parenthesised quantified antecedent at the start of a statement is + /// read as a binder telescope (`forall` and `x` become bound names and + /// only `Q` is left). The key is unchanged; it is reported incomplete. + #[test] + fn telescope_misread_of_a_quantified_antecedent_is_incomplete() { + let k = structural_key("(forall x : nat, P x) -> Q"); + assert_eq!(k.shape, "(PI [NAT NAT] v0)", "the behaviour this flags"); + assert!(!k.complete); + // A real telescope is still complete. + assert!(structural_key("(x y : nat) : x + y = y + x").complete); + } + /// The guard is a no-op on balanced input: keys stay as they were. #[test] fn balanced_input_keys_are_unchanged_by_the_bracket_guard() { From 0f5ba8ae75d4e48797d836c3cfb733c3d91ff15c Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 27 Oct 2026 04:22:15 +0000 Subject: [PATCH 03/16] feat(lexicon): echidna lexicon scan mines cross-corpus candidates (stage 6c PR 3) Compares training_data/ corpora by theorem name and by canonical statement shape (corpus::canonical, dk-shape-v1). Same name and same shape is a cognate; same name and a different shape is a false friend or a specialisation (cognate_skeleton when only the skeleton agrees); a different name with identical text, the same shape or the same skeleton is a synonym candidate. Pairs where either side was not read completely are `unparsed`, and incomplete keys take no part in shape joins. Joins between different names skip shapes too thin to identify anything (a variable in function position, fewer than three constants, a bare type signature); every skip and cap is counted. Output is I-JSON serialised as JCS, one record per line, under target/lexicon-scan: pairs/__.jsonl, summary.jsonl, coverage.jsonl and sampled key collisions. Each candidate's id is the UUIDv8 content id of the statement pair, independent of scan direction and normaliser version. Every record carries evidence = none, and data/synonyms/ is never written (D4). Presets: learning, spanning (one corpus per family), in-family and full (33 pairs); a full run takes about three minutes on a debug build. The design used #449's canonicaliser instead of building a separate lexical normaliser, a departure from the 2026-10-20 plan recorded in the ADR. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01WS4mfQeC3N1DWjcCQJaQqw --- Justfile | 8 + data/synonyms/README.adoc | 41 +- src/rust/lexicon/mod.rs | 13 + src/rust/lexicon/scan.rs | 1211 +++++++++++++++++ src/rust/lib.rs | 1 + src/rust/main.rs | 166 +++ .../scan/proof_states_hol4_mini.jsonl | 6 + .../scan/proof_states_hol_light_mini.jsonl | 5 + .../scan/proof_states_isabelle_mini.jsonl | 8 + .../scan/proof_states_lean_mini.jsonl | 9 + tests/lexicon_scan_test.rs | 201 +++ 11 files changed, 1667 insertions(+), 2 deletions(-) create mode 100644 src/rust/lexicon/mod.rs create mode 100644 src/rust/lexicon/scan.rs create mode 100644 tests/lexicon_fixtures/scan/proof_states_hol4_mini.jsonl create mode 100644 tests/lexicon_fixtures/scan/proof_states_hol_light_mini.jsonl create mode 100644 tests/lexicon_fixtures/scan/proof_states_isabelle_mini.jsonl create mode 100644 tests/lexicon_fixtures/scan/proof_states_lean_mini.jsonl create mode 100644 tests/lexicon_scan_test.rs diff --git a/Justfile b/Justfile index a9b57888..6b82224c 100644 --- a/Justfile +++ b/Justfile @@ -1163,6 +1163,14 @@ lexicon-check: scripts/lexicon-check.sh cargo test --locked --test lexicon_v2_test +# Mine lexicon candidates across training_data/ corpora: cognates, false +# friends and synonym candidates as JCS JSON Lines under target/lexicon-scan. +# Flag-only (evidence = none); never edits data/synonyms/. Presets: learning, +# spanning, in-family, full. +lexicon-scan preset="learning": + cargo run --locked --bin echidna -- lexicon scan --preset {{preset}} + cargo test --locked --test lexicon_scan_test + # Run the saturation-campaign cargo tests only (139 cases + 1 ignored). test-saturation: cargo test --lib -- \ diff --git a/data/synonyms/README.adoc b/data/synonyms/README.adoc index 54e32a44..0a9af866 100644 --- a/data/synonyms/README.adoc +++ b/data/synonyms/README.adoc @@ -219,6 +219,42 @@ Nickel contract `schema.ncl`; `scripts/lexicon-check.sh` (or Corpus-mined candidates (owner decision D4) are flag-only: they carry `evidence = { kind = "none" }` and never set `semantic_class` on their own. +=== Mining candidates: `echidna lexicon scan` + +`echidna lexicon scan --preset learning` (or `just lexicon-scan`) compares +`training_data/proof_states_.jsonl` corpora on two axes, the theorem +*name* and the canonical *shape* of its statement (`dk-shape-v1`, +`src/rust/corpus/canonical.rs`), and writes review candidates as JCS JSON +Lines under `target/lexicon-scan/`. It never edits this directory. + +[cols="1,2,2"] +|=== +| | same shape | different shape + +| *same name* +| cognate (`cognate_exact`, `cognate_shape`) +| false friend or specialisation (`cognate_skeleton`, `differs`) + +| *different name* +| synonym candidate (joins `text`, `shape`, `skeleton`) +| unrelated, not reported +|=== + +A pair is `unparsed` when either statement was not read completely by the +canonicaliser (`StructuralKey::complete`): its key is then a prefix that +other statements share, so it says nothing. Joins between different names +also skip shapes too thin to identify anything (`informative`: a variable in +function position, fewer than three constants, or a bare type signature). +Every skip is counted in `summary.jsonl`; `coverage.jsonl` reports, per +corpus, how much the canonicaliser read and how often distinct statements +share a key. Each candidate's `id` is the UUIDv8 content id of the +statement pair, independent of scan direction and normaliser version, so a +review decision survives a re-scan. + +A candidate becomes a row here only by curation: a person writes the row +with `evidence = curated` (or `probe` / `kernel` once that evidence exists), +and the Nickel contract checks it like any other. + Nickel checks shape and the cross-field rules; serde checks that `checked_by` names a `ProverKind` and `format` an `ExchangeFormat` when Rust loads a table (`tests/lexicon_v2_test.rs`). @@ -242,8 +278,9 @@ prover no longer accepts (or never accepted in this version). - Cross-prover synonym graph (Isabelle `le_trans` ↔ Coq `Rle_trans` ↔ Lean `le_trans`) is intentionally **out of scope** here — that's `echidna port`, not `echidna suggest`. -- ML-driven synonym discovery from the corpus (mining - `training_data/`) is in §4.4 of the notes, not this layer. +- ML-driven synonym discovery from the corpus is in §4.4 of the notes, + not this layer. Syntactic mining of `training_data/` is + `echidna lexicon scan` (above); it proposes, it never writes here. == Maintenance diff --git a/src/rust/lexicon/mod.rs b/src/rust/lexicon/mod.rs new file mode 100644 index 00000000..a81923f6 --- /dev/null +++ b/src/rust/lexicon/mod.rs @@ -0,0 +1,13 @@ +// SPDX-License-Identifier: MPL-2.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) + +//! Lexicon tooling that works *on* corpora rather than on one synonym table. +//! +//! The synonym tables themselves (`data/synonyms/*.toml`, loaded by +//! [`crate::suggest::synonyms`]) are curated by hand under the Nickel +//! contract `data/synonyms/schema.ncl`. This module only *proposes*: it +//! mines the training corpora for rows a curator may want to add, and every +//! proposal carries `evidence = none` (owner decision D4 in +//! `docs/decisions/2026-10-19-lexicon-v2-and-identity-arbitration.adoc`). + +pub mod scan; diff --git a/src/rust/lexicon/scan.rs b/src/rust/lexicon/scan.rs new file mode 100644 index 00000000..241fde99 --- /dev/null +++ b/src/rust/lexicon/scan.rs @@ -0,0 +1,1211 @@ +// SPDX-License-Identifier: MPL-2.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) + +//! `echidna lexicon scan`: a cross-corpus candidate generator for the lexicon. +//! +//! Two corpora are compared along two axes, the *name* of a theorem and the +//! canonical *shape* of its statement ([`crate::corpus::canonical`], scheme +//! `dk-shape-v1`). The four combinations are the four things a curator +//! wants to know about: +//! +//! | | same shape | different shape | +//! |---|---|---| +//! | **same name** | cognate | false friend, or specialisation | +//! | **different name** | synonym candidate | unrelated (not reported) | +//! +//! A pair joined by name is classified by the strongest tier at which its two +//! statements agree: identical text (`cognate_exact`), the same structural +//! key (`cognate_shape`: same shape up to variable names), the same skeleton +//! key only (`cognate_skeleton`: the shapes differ in binders or sorts, the +//! usual signature of a specialisation such as `nat` against `real`), or +//! none (`differs`). A pair joined by identical text, by shape, or failing +//! those by skeleton has different names and is a synonym candidate; the +//! text join needs no canonicaliser at all. +//! +//! Shape classification needs both statements read *completely* +//! ([`StructuralKey::complete`]). `dk-shape-v1` still returns a +//! structural-tier key when its parser stops early or meets notation it has +//! no rule for (HOL binders, Isabelle `\<…>` escapes), and that key is a +//! prefix many different statements share. Such pairs are `unparsed`, and +//! such statements take no part in shape or skeleton joins. +//! +//! None of this is evidence. The canonical shape is a syntactic key, not a +//! decision procedure; `dk-shape-v1` documents what it does not normalise, +//! and [`Coverage`] measures how much of each corpus it actually reads and +//! how often distinct statements collide on one key. Every candidate is +//! written with `evidence = { kind = "none" }` and never edits +//! `data/synonyms/` (owner decision D4). +//! +//! Output is I-JSON serialised as JCS (RFC 8785), one record per line, so +//! records hash and diff stably. Each candidate's `id` is the UUIDv8 content +//! id ([`crate::ids::content_id`]) of the statement pair alone, with the two +//! sides in a fixed order: the same pair keeps the same id whichever corpus +//! is named first and whichever normaliser version classified it, so a +//! curator's review survives a re-scan. + +use std::collections::{BTreeMap, BTreeSet, HashMap}; +use std::fs::{self, File}; +use std::io::{BufRead, BufReader, BufWriter, Write}; +use std::path::{Path, PathBuf}; +use std::time::{Duration, Instant}; + +use anyhow::{bail, Context, Result}; +use serde::Serialize; + +use crate::corpus::canonical::{self, KeyTier, StructuralKey}; +use crate::suggest::synonyms::LexiconEvidence; + +/// Schema tag of one candidate record. +pub const CANDIDATE_SCHEMA: &str = "echidna.lexicon.candidate/1"; +/// Schema tag of one per-pair summary record. +pub const PAIR_SUMMARY_SCHEMA: &str = "echidna.lexicon.pair-summary/1"; +/// Schema tag of one per-corpus coverage record. +pub const COVERAGE_SCHEMA: &str = "echidna.lexicon.coverage/1"; +/// Schema tag of one sampled key-collision group. +pub const COLLISION_SCHEMA: &str = "echidna.lexicon.collision/1"; + +/// One corpus per prover family, the cross-family spanning set: classical +/// higher-order logic (HOL4), Isabelle/HOL (the AFP), dependent type theory +/// (Lean 3), set theory (Mizar), first-order computational logic (ACL2), +/// auto-active verification (Why3), logic programming (λProlog) and the +/// λΠ-modulo hub (Dedukti). +pub const SPANNING: [&str; 8] = [ + "hol4", + "afp", + "lean3", + "mizar", + "acl2", + "why3", + "lambda_prolog", + "dedukti", +]; + +/// One pair inside each family that has a second corpus, so differences +/// within a family can be told apart from differences across families. +pub const IN_FAMILY: [(&str, &str); 5] = [ + ("hol4", "hol_light"), + ("lean3", "agda"), + ("acl2", "acl2s"), + ("why3", "dafny"), + ("mizar", "isabelle_zf"), +]; + +/// The two pairs read first: the stage-6a pilot pair inside the HOL family, +/// and the cross-family pair with the most shared names. +pub const LEARNING: [(&str, &str); 2] = [("hol4", "hol_light"), ("lean3", "afp")]; + +/// The pairs a named preset expands to, in scan order, or `None` for an +/// unknown preset. `full` is every spanning pair followed by the in-family +/// pairs. +pub fn preset_pairs(preset: &str) -> Option> { + let owned = |pairs: &[(&str, &str)]| { + pairs + .iter() + .map(|(a, b)| (a.to_string(), b.to_string())) + .collect::>() + }; + let spanning = || { + let mut out = Vec::new(); + for (i, a) in SPANNING.iter().enumerate() { + for b in &SPANNING[i + 1..] { + out.push((a.to_string(), b.to_string())); + } + } + out + }; + match preset { + "learning" => Some(owned(&LEARNING)), + "spanning" => Some(spanning()), + "in-family" => Some(owned(&IN_FAMILY)), + "full" => { + let mut out = spanning(); + out.extend(owned(&IN_FAMILY)); + Some(out) + }, + _ => None, + } +} + +/// Parse a `A:B` pair argument. Both sides must be corpus keys as they +/// appear in `proof_states_.jsonl`. +pub fn parse_pair(arg: &str) -> Result<(String, String)> { + let (a, b) = arg + .split_once(':') + .with_context(|| format!("pair `{arg}` must be written A:B"))?; + validate_corpus_key(a)?; + validate_corpus_key(b)?; + if a == b { + bail!("pair `{arg}` names the same corpus twice"); + } + Ok((a.to_string(), b.to_string())) +} + +/// Corpus keys become file names, so only `[a-z0-9_]` is accepted. +pub fn validate_corpus_key(key: &str) -> Result<()> { + if key.is_empty() + || !key + .chars() + .all(|c| c.is_ascii_lowercase() || c.is_ascii_digit() || c == '_') + { + bail!("corpus key `{key}` must be non-empty [a-z0-9_]"); + } + Ok(()) +} + +/// Fold a theorem name for cross-prover matching: keep the last component +/// of a dotted or `::`-qualified name, lower-case it, read `-` as `_`, and +/// trim surrounding underscores. `nat.add_comm`, `ADD_COMM` and `add-comm` +/// all fold to `add_comm`. +pub fn fold_name(name: &str) -> String { + let tail = name.rsplit(['.', ':']).next().unwrap_or(name); + let tail = if tail.is_empty() { name } else { tail }; + tail.to_lowercase() + .replace('-', "_") + .trim_matches('_') + .to_string() +} + +/// Folded names that say nothing about the statement: numbered lemmas, +/// examples, auxiliaries, Mizar's anonymous theorems and any stem of two +/// characters or fewer once trailing digits, primes and underscores are +/// removed (`l3`, `th27`, `ex1`, `z`). +const GENERIC_STEMS: [&str; 34] = [ + "anonymous", + "aux", + "auxiliary", + "bar", + "base", + "baz", + "case", + "claim", + "cor", + "corollary", + "def", + "defn", + "example", + "exercise", + "fact", + "foo", + "goal", + "helper", + "ind", + "key", + "lem", + "lemma", + "main", + "prop", + "remark", + "result", + "step", + "sublemma", + "temp", + "test", + "thm", + "theorem", + "tmp", + "unnamed", +]; + +/// Whether a folded name is too generic to join two corpora on. +pub fn is_generic(folded: &str) -> bool { + let stem = folded.trim_end_matches(|c: char| c.is_ascii_digit() || c == '\'' || c == '_'); + stem.chars().count() <= 2 || GENERIC_STEMS.contains(&stem) +} + +/// One distinct `(name, statement)` row of a corpus. +#[derive(Debug, Clone)] +pub struct Entry { + pub name: String, + /// The statement with runs of whitespace collapsed to one space. + pub statement: String, + key: usize, +} + +/// A training corpus, deduplicated and indexed for the scan. +#[derive(Debug, Clone)] +pub struct Corpus { + pub key: String, + /// Distinct rows, sorted by name then statement. + pub entries: Vec, + keys: Vec, + pub lines_read: usize, + /// Lines that are not JSON objects. + pub lines_malformed: usize, + /// Objects without a non-empty string `theorem` and `goal`. + pub lines_without_statement: usize, + by_name: BTreeMap>, + by_fold: BTreeMap>, + by_statement: BTreeMap>, + by_shape: BTreeMap>, + by_skeleton: BTreeMap>, +} + +fn collapse_whitespace(s: &str) -> String { + s.split_whitespace().collect::>().join(" ") +} + +impl Corpus { + /// Build a corpus from `(name, statement)` rows. Names are trimmed, + /// statement whitespace is collapsed, and rows with an empty side or a + /// duplicate of an earlier row are dropped. + pub fn from_rows(key: &str, rows: I) -> Self + where + I: IntoIterator, + { + let distinct: BTreeSet<(String, String)> = rows + .into_iter() + .map(|(n, s)| (n.trim().to_string(), collapse_whitespace(&s))) + .filter(|(n, s)| !n.is_empty() && !s.is_empty()) + .collect(); + + let mut keys: Vec = Vec::new(); + let mut key_of: HashMap = HashMap::new(); + let mut entries = Vec::with_capacity(distinct.len()); + for (name, statement) in distinct { + let k = match key_of.get(&statement) { + Some(&k) => k, + None => { + keys.push(canonical::structural_key(&statement)); + key_of.insert(statement.clone(), keys.len() - 1); + keys.len() - 1 + }, + }; + entries.push(Entry { + name, + statement, + key: k, + }); + } + + let mut by_name: BTreeMap> = BTreeMap::new(); + let mut by_fold: BTreeMap> = BTreeMap::new(); + let mut by_shape: BTreeMap> = BTreeMap::new(); + let mut by_statement: BTreeMap> = BTreeMap::new(); + let mut by_skeleton: BTreeMap> = BTreeMap::new(); + for (i, e) in entries.iter().enumerate() { + by_name.entry(e.name.clone()).or_default().push(i); + by_statement.entry(e.statement.clone()).or_default().push(i); + let folded = fold_name(&e.name); + if !folded.is_empty() { + by_fold.entry(folded).or_default().insert(e.name.clone()); + } + // Only a complete parse can stand for its statement in a join; + // an incomplete shape is a prefix that other statements share. + let k = &keys[e.key]; + if !k.complete { + continue; + } + if k.tier == KeyTier::Structural { + by_shape.entry(k.key.clone()).or_default().push(i); + } + if !k.skeleton.is_empty() { + by_skeleton + .entry(k.skeleton_key.clone()) + .or_default() + .push(i); + } + } + + Corpus { + key: key.to_string(), + entries, + keys, + lines_read: 0, + lines_malformed: 0, + lines_without_statement: 0, + by_name, + by_statement, + by_fold, + by_shape, + by_skeleton, + } + } + + /// Load `training_dir/proof_states_.jsonl`, reading each line's + /// `theorem` and `goal` strings. + /// + /// # Errors + /// + /// The key is not `[a-z0-9_]`, or the file is missing, unreadable, not + /// UTF-8, or holds no usable row. Lines that are not JSON objects, or + /// lack a string `theorem` or `goal`, are counted rather than fatal. + pub fn load(training_dir: &Path, key: &str) -> Result { + validate_corpus_key(key)?; + let path = training_dir.join(format!("proof_states_{key}.jsonl")); + let file = File::open(&path).with_context(|| format!("open {}", path.display()))?; + let reader = BufReader::new(file); + let mut rows = Vec::new(); + let (mut read, mut malformed, mut without) = (0usize, 0usize, 0usize); + for line in reader.lines() { + let line = line.with_context(|| format!("read {}", path.display()))?; + if line.trim().is_empty() { + continue; + } + read += 1; + let value: serde_json::Value = match serde_json::from_str(&line) { + Ok(v) => v, + Err(_) => { + malformed += 1; + continue; + }, + }; + let field = |f: &str| value.get(f).and_then(serde_json::Value::as_str); + match (field("theorem"), field("goal")) { + (Some(t), Some(g)) if !t.trim().is_empty() && !g.trim().is_empty() => { + rows.push((t.to_string(), g.to_string())); + }, + _ => without += 1, + } + } + let mut corpus = Corpus::from_rows(key, rows); + if corpus.entries.is_empty() { + bail!("{}: no usable (theorem, goal) rows", path.display()); + } + corpus.lines_read = read; + corpus.lines_malformed = malformed; + corpus.lines_without_statement = without; + Ok(corpus) + } + + fn key_of(&self, i: usize) -> &StructuralKey { + &self.keys[self.entries[i].key] + } + + /// Distinct names that carry more than one distinct statement. + pub fn homonym_names(&self) -> usize { + self.by_name.values().filter(|v| v.len() > 1).count() + } + + /// How much of the corpus the canonicaliser keyed at each tier, and how + /// often distinct statements share one structural key. + pub fn coverage(&self) -> Coverage { + let mut tiers = TierCounts::default(); + for e in &self.entries { + let k = &self.keys[e.key]; + match k.tier { + KeyTier::Structural => tiers.structural += 1, + KeyTier::Skeleton => tiers.skeleton += 1, + KeyTier::Text => tiers.text += 1, + } + if k.complete { + tiers.complete += 1; + } + } + let (mut collision_keys, mut collision_statements) = (0usize, 0usize); + for group in self.by_shape.values() { + let texts = self.distinct_statements(group); + if texts > 1 { + collision_keys += 1; + collision_statements += texts; + } + } + Coverage { + schema: COVERAGE_SCHEMA, + scheme: canonical::SCHEME, + corpus: self.key.clone(), + lines_read: self.lines_read, + lines_malformed: self.lines_malformed, + lines_without_statement: self.lines_without_statement, + rows: self.entries.len(), + names: self.by_name.len(), + homonym_names: self.homonym_names(), + tiers, + collision_keys, + collision_statements, + } + } + + fn distinct_statements(&self, group: &[usize]) -> usize { + group + .iter() + .map(|&i| self.entries[i].statement.as_str()) + .collect::>() + .len() + } + + /// Sample structural keys that distinct statements share: half the + /// sample from the largest groups (trivial shapes), half from groups of + /// exactly two (where a false merge is easiest to read). Each group lists + /// at most six members. + pub fn collisions(&self, limit: usize) -> Vec { + let mut multi: Vec<(&String, &Vec, usize)> = self + .by_shape + .iter() + .map(|(k, g)| (k, g, self.distinct_statements(g))) + .filter(|(_, _, n)| *n > 1) + .collect(); + let mut picked: Vec<(&String, &Vec, usize)> = Vec::new(); + let mut largest = multi.clone(); + largest.sort_by(|x, y| y.2.cmp(&x.2).then_with(|| x.0.cmp(y.0))); + picked.extend(largest.into_iter().take(limit / 2)); + multi.retain(|(k, _, n)| *n == 2 && !picked.iter().any(|(pk, _, _)| pk == k)); + picked.extend(multi.into_iter().take(limit - picked.len().min(limit))); + + picked + .into_iter() + .map(|(key, group, n)| { + let mut seen = BTreeSet::new(); + let members = group + .iter() + .filter(|&&i| seen.insert(self.entries[i].statement.clone())) + .take(6) + .map(|&i| Member { + name: self.entries[i].name.clone(), + statement: self.entries[i].statement.clone(), + }) + .collect(); + CollisionRecord { + schema: COLLISION_SCHEMA, + scheme: canonical::SCHEME, + corpus: self.key.clone(), + key: key.clone(), + shape: self.key_of(group[0]).shape.clone(), + distinct_statements: n, + members, + } + }) + .collect() + } +} + +/// Entries keyed at each canonicalisation tier, and how many of them the +/// parser read completely ([`StructuralKey::complete`]). +#[derive(Debug, Clone, Default, PartialEq, Eq, Serialize)] +pub struct TierCounts { + pub structural: usize, + pub skeleton: usize, + pub text: usize, + pub complete: usize, +} + +/// Per-corpus parse coverage and key-collision counts. +#[derive(Debug, Clone, Serialize)] +pub struct Coverage { + pub schema: &'static str, + pub scheme: &'static str, + pub corpus: String, + pub lines_read: usize, + pub lines_malformed: usize, + pub lines_without_statement: usize, + /// Distinct `(name, statement)` rows. + pub rows: usize, + pub names: usize, + /// Names with more than one distinct statement. + pub homonym_names: usize, + pub tiers: TierCounts, + /// Structural keys shared by two or more distinct statement texts: + /// alpha-variants of one statement, or distinct statements the scheme + /// cannot tell apart. + pub collision_keys: usize, + /// Distinct statements inside those keys. + pub collision_statements: usize, +} + +/// One name and statement inside a sampled collision group. +#[derive(Debug, Clone, Serialize)] +pub struct Member { + pub name: String, + pub statement: String, +} + +/// A structural key that distinct statements share, for review. +#[derive(Debug, Clone, Serialize)] +pub struct CollisionRecord { + pub schema: &'static str, + pub scheme: &'static str, + pub corpus: String, + pub key: String, + pub shape: String, + pub distinct_statements: usize, + pub members: Vec, +} + +/// How a candidate pair was found. +#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Serialize)] +#[serde(rename_all = "snake_case")] +pub enum Join { + /// The same theorem name in both corpora. + NameExact, + /// Names equal after [`fold_name`] but not before. + NameFolded, + /// Different names, identical statement text. Needs no canonicaliser, + /// so it also finds synonyms among statements `dk-shape-v1` cannot read. + Text, + /// Different names, the same structural key. + Shape, + /// Different names, the same skeleton key and a different structural key. + Skeleton, +} + +/// The strongest tier at which a pair's statements agree. +#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Serialize)] +#[serde(rename_all = "snake_case")] +pub enum Candidate { + /// Identical text after whitespace collapsing. + CognateExact, + /// Different text, the same structural key: equal up to variable names + /// and the spellings `dk-shape-v1` normalises. + CognateShape, + /// Only the skeleton keys agree: the statements differ in binders or + /// sorts. For a name join this is a specialisation candidate. + CognateSkeleton, + /// Both statements parsed completely and no key agrees: a false friend + /// or a specialisation the scheme cannot see. Only a probe or a kernel + /// can tell which. + Differs, + /// The texts differ and at least one side did not parse completely, so + /// the keys say nothing either way. + Unparsed, +} + +/// One side of a candidate pair. +#[derive(Debug, Clone, Serialize)] +pub struct Side { + pub corpus: String, + pub name: String, + pub statement: String, + /// `structural`, `skeleton` or `text`: how far the canonicaliser got. + pub tier: &'static str, + /// Whether the canonicaliser read the whole statement; when `false` the + /// shape is a prefix and takes no part in shape classification. + pub complete: bool, + /// The canonical shape at that tier (normalised text for `text`). + pub shape: String, +} + +/// One review candidate. Never evidence: `evidence` is always `none`. +#[derive(Debug, Clone, Serialize)] +pub struct CandidateRecord { + pub schema: &'static str, + /// UUIDv8 content id of the statement pair (see the module docs). + pub id: String, + pub scheme: &'static str, + pub join: Join, + pub candidate: Candidate, + pub a: Side, + pub b: Side, + /// Jaccard similarity, in thousandths, of the two shapes' constant and + /// operator atoms (variables `v0`, `v1`, … and `PI` excluded). A ranking + /// aid for review, not a measure of sameness. + pub similarity_permille: u32, + /// The shared name is generic (only with `--keep-generic`). + pub generic_name: bool, + pub evidence: LexiconEvidence, +} + +/// Counts of candidates by classification. +#[derive(Debug, Clone, Default, PartialEq, Eq, Serialize)] +pub struct CandidateCounts { + pub cognate_exact: usize, + pub cognate_shape: usize, + pub cognate_skeleton: usize, + pub differs: usize, + pub unparsed: usize, +} + +impl CandidateCounts { + fn add(&mut self, c: Candidate) { + match c { + Candidate::CognateExact => self.cognate_exact += 1, + Candidate::CognateShape => self.cognate_shape += 1, + Candidate::CognateSkeleton => self.cognate_skeleton += 1, + Candidate::Differs => self.differs += 1, + Candidate::Unparsed => self.unparsed += 1, + } + } + + pub fn total(&self) -> usize { + self.cognate_exact + + self.cognate_shape + + self.cognate_skeleton + + self.differs + + self.unparsed + } +} + +/// Candidate counts for each join. +#[derive(Debug, Clone, Default, PartialEq, Eq, Serialize)] +pub struct JoinCounts { + pub name_exact: CandidateCounts, + pub name_folded: CandidateCounts, + pub text: CandidateCounts, + pub shape: CandidateCounts, + pub skeleton: CandidateCounts, +} + +impl JoinCounts { + fn add(&mut self, join: Join, c: Candidate) { + match join { + Join::NameExact => self.name_exact.add(c), + Join::NameFolded => self.name_folded.add(c), + Join::Text => self.text.add(c), + Join::Shape => self.shape.add(c), + Join::Skeleton => self.skeleton.add(c), + } + } +} + +/// What one pair scan found and what it skipped. +#[derive(Debug, Clone, Serialize)] +pub struct PairSummary { + pub schema: &'static str, + pub scheme: &'static str, + pub pair: [String; 2], + /// Folded names present in both corpora. + pub folded_names_shared: usize, + /// Of those, the generic ones not emitted (see [`is_generic`]). + pub generic_names_skipped: usize, + /// Raw-name pairs whose statement cross product exceeded the cap. + pub name_pairs_capped: usize, + /// Statement pairs inside those capped name pairs. + pub statement_pairs_capped: usize, + /// Identical-text groups over the size cap on either side, or too short + /// (fewer than three tokens) to join two names on. + pub text_groups_capped: usize, + pub text_groups_uninformative: usize, + /// Shape or skeleton groups over the size cap on either side. + pub shape_groups_capped: usize, + pub skeleton_groups_capped: usize, + /// Shape or skeleton groups shared by both corpora but skipped as too + /// little structure for a synonym (see [`informative`]). + pub shape_groups_uninformative: usize, + pub skeleton_groups_uninformative: usize, + pub candidates: JoinCounts, +} + +/// Limits that keep a scan's output reviewable. +#[derive(Debug, Clone)] +pub struct ScanOptions { + /// Emit pairs whose shared name is generic. + pub keep_generic: bool, + /// Skip a shared name whose statement cross product exceeds this. + pub max_pairs_per_name: usize, + /// Skip a shape or skeleton group larger than this on either side. + pub max_shape_group: usize, +} + +impl Default for ScanOptions { + fn default() -> Self { + ScanOptions { + keep_generic: false, + max_pairs_per_name: 64, + max_shape_group: 8, + } + } +} + +fn atoms(shape: &str) -> BTreeSet<&str> { + shape + .split(|c: char| c.is_whitespace() || matches!(c, '(' | ')' | '[' | ']')) + .filter(|t| !t.is_empty() && *t != "PI") + .filter(|t| { + !(t.len() > 1 && t.starts_with('v') && t[1..].chars().all(|c| c.is_ascii_digit())) + }) + .collect() +} + +/// Canonical sort atoms (`dk-shape-v1`'s `sort_of`) plus `ARROW`: the type +/// language. A shape made only of these and variables is a bare signature. +const TYPE_ATOMS: [&str; 9] = [ + "ARROW", "NAT", "INT", "BOOL", "REAL", "TYPE", "STRING", "LIST", "VEC", +]; + +/// Whether a skeleton carries enough structure to propose a synonym between +/// two *differently named* statements: at least three non-variable atoms, +/// at least one of them outside the type language, and no variable applied +/// to arguments. `dk-shape-v1` renames any short lower-case name to a +/// variable, so `cos 0 = 1`, `exp 0 = 1` and `n 0 = 1` all become +/// `(EQ (v0 0) 1)`; a variable in function position is the mark of that. +/// A bare `(summable v0)` says only that something is summable, and a bare +/// signature such as `int -> int -> int` is shared by every function of +/// that type. Name joins are not filtered: there the shared name anchors. +pub fn informative(skeleton: &str) -> bool { + let chars: Vec = skeleton.chars().collect(); + let variable_head = chars.windows(3).enumerate().any(|(i, w)| { + w[0] == '(' && w[1] == 'v' && w[2].is_ascii_digit() && { + let rest = &chars[i + 2..]; + let digits = rest.iter().take_while(|c| c.is_ascii_digit()).count(); + matches!(rest.get(digits), Some(' ')) + } + }); + let constants: Vec<&str> = skeleton + .split(|c: char| c.is_whitespace() || matches!(c, '(' | ')' | '[' | ']')) + // `?` is an erased sort and `_` a hole: placeholders, not atoms. + .filter(|t| !t.is_empty() && !matches!(*t, "PI" | "?" | "_")) + .filter(|t| { + !(t.len() > 1 && t.starts_with('v') && t[1..].chars().all(|c| c.is_ascii_digit())) + }) + .collect(); + let beyond_types = constants.iter().any(|t| !TYPE_ATOMS.contains(t)); + !variable_head && constants.len() >= 3 && beyond_types +} + +fn similarity_permille(a: &str, b: &str) -> u32 { + let (sa, sb) = (atoms(a), atoms(b)); + let union = sa.union(&sb).count(); + if union == 0 { + return 0; + } + (sa.intersection(&sb).count() * 1000 / union) as u32 +} + +fn classify(a: &Entry, ka: &StructuralKey, b: &Entry, kb: &StructuralKey) -> Candidate { + if a.statement == b.statement { + return Candidate::CognateExact; + } + // `complete` is false at the text tier, so this also covers unparsed text. + if !ka.complete || !kb.complete { + return Candidate::Unparsed; + } + if ka.tier == KeyTier::Structural && kb.tier == KeyTier::Structural && ka.key == kb.key { + return Candidate::CognateShape; + } + if !ka.skeleton.is_empty() && ka.skeleton_key == kb.skeleton_key { + return Candidate::CognateSkeleton; + } + Candidate::Differs +} + +#[derive(Serialize)] +struct IdSide<'s> { + corpus: &'s str, + name: &'s str, + statement: &'s str, +} + +#[derive(Serialize)] +struct IdPair<'s> { + a: IdSide<'s>, + b: IdSide<'s>, +} + +/// The order-independent content id of a statement pair. +pub fn pair_id( + (ca, na, sa): (&str, &str, &str), + (cb, nb, sb): (&str, &str, &str), +) -> Result { + let x = IdSide { + corpus: ca, + name: na, + statement: sa, + }; + let y = IdSide { + corpus: cb, + name: nb, + statement: sb, + }; + let pair = if (ca, na, sa) <= (cb, nb, sb) { + IdPair { a: x, b: y } + } else { + IdPair { a: y, b: x } + }; + Ok(crate::ids::content_id(&pair)?.to_string()) +} + +fn side(c: &Corpus, i: usize) -> Side { + let e = &c.entries[i]; + let k = c.key_of(i); + Side { + corpus: c.key.clone(), + name: e.name.clone(), + statement: e.statement.clone(), + tier: k.tier.as_str(), + complete: k.complete, + shape: k.shape.clone(), + } +} + +fn record( + a: &Corpus, + ia: usize, + b: &Corpus, + ib: usize, + join: Join, + candidate: Candidate, + generic_name: bool, +) -> Result { + let (ea, eb) = (&a.entries[ia], &b.entries[ib]); + Ok(CandidateRecord { + schema: CANDIDATE_SCHEMA, + id: pair_id( + (a.key.as_str(), ea.name.as_str(), ea.statement.as_str()), + (b.key.as_str(), eb.name.as_str(), eb.statement.as_str()), + )?, + scheme: canonical::SCHEME, + join, + candidate, + a: side(a, ia), + b: side(b, ib), + similarity_permille: similarity_permille(&a.key_of(ia).shape, &b.key_of(ib).shape), + generic_name, + evidence: LexiconEvidence::None, + }) +} + +/// Scan one corpus pair, passing every candidate to `emit` in a fixed +/// order: name joins by folded name, then text, shape and skeleton joins, +/// each by key. A pair is reported by the first join that finds it. +/// +/// # Errors +/// +/// Whatever `emit` returns, or a failure to derive a content id. +pub fn scan_pair( + a: &Corpus, + b: &Corpus, + opts: &ScanOptions, + emit: &mut dyn FnMut(&CandidateRecord) -> Result<()>, +) -> Result { + let mut summary = PairSummary { + schema: PAIR_SUMMARY_SCHEMA, + scheme: canonical::SCHEME, + pair: [a.key.clone(), b.key.clone()], + folded_names_shared: 0, + generic_names_skipped: 0, + name_pairs_capped: 0, + statement_pairs_capped: 0, + text_groups_capped: 0, + text_groups_uninformative: 0, + shape_groups_capped: 0, + skeleton_groups_capped: 0, + shape_groups_uninformative: 0, + skeleton_groups_uninformative: 0, + candidates: JoinCounts::default(), + }; + + // 1. Name joins: same folded name. + for (folded, names_a) in &a.by_fold { + let Some(names_b) = b.by_fold.get(folded) else { + continue; + }; + summary.folded_names_shared += 1; + let generic = is_generic(folded); + if generic && !opts.keep_generic { + summary.generic_names_skipped += 1; + continue; + } + for na in names_a { + for nb in names_b { + let (ga, gb) = (&a.by_name[na], &b.by_name[nb]); + let product = ga.len() * gb.len(); + if product > opts.max_pairs_per_name { + summary.name_pairs_capped += 1; + summary.statement_pairs_capped += product; + continue; + } + let join = if na == nb { + Join::NameExact + } else { + Join::NameFolded + }; + for &ia in ga { + for &ib in gb { + let c = + classify(&a.entries[ia], a.key_of(ia), &b.entries[ib], b.key_of(ib)); + summary.candidates.add(join, c); + emit(&record(a, ia, b, ib, join, c, generic)?)?; + } + } + } + } + } + + let same_name = + |ia: usize, ib: usize| fold_name(&a.entries[ia].name) == fold_name(&b.entries[ib].name); + let same_text = |ia: usize, ib: usize| a.entries[ia].statement == b.entries[ib].statement; + + // 2. Text joins: different names, identical statement text. A statement + // of fewer than three tokens (`T`, `x = y`) says too little to join on. + for (text, ga) in &a.by_statement { + let Some(gb) = b.by_statement.get(text) else { + continue; + }; + if ga.len() > opts.max_shape_group || gb.len() > opts.max_shape_group { + summary.text_groups_capped += 1; + continue; + } + if text.split_whitespace().count() < 3 { + summary.text_groups_uninformative += 1; + continue; + } + for &ia in ga { + for &ib in gb { + if same_name(ia, ib) { + continue; + } + summary.candidates.add(Join::Text, Candidate::CognateExact); + emit(&record( + a, + ia, + b, + ib, + Join::Text, + Candidate::CognateExact, + false, + )?)?; + } + } + } + + // 3. Shape joins: different names, the same structural key, and not + // already joined by text. + for (key, ga) in &a.by_shape { + let Some(gb) = b.by_shape.get(key) else { + continue; + }; + if ga.len() > opts.max_shape_group || gb.len() > opts.max_shape_group { + summary.shape_groups_capped += 1; + continue; + } + if !informative(&a.key_of(ga[0]).skeleton) { + summary.shape_groups_uninformative += 1; + continue; + } + for &ia in ga { + for &ib in gb { + if same_name(ia, ib) || same_text(ia, ib) { + continue; + } + let c = classify(&a.entries[ia], a.key_of(ia), &b.entries[ib], b.key_of(ib)); + summary.candidates.add(Join::Shape, c); + emit(&record(a, ia, b, ib, Join::Shape, c, false)?)?; + } + } + } + + // 4. Skeleton joins: different names, the same skeleton key, and not + // already joined by text or shape. + for (key, ga) in &a.by_skeleton { + let Some(gb) = b.by_skeleton.get(key) else { + continue; + }; + if ga.len() > opts.max_shape_group || gb.len() > opts.max_shape_group { + summary.skeleton_groups_capped += 1; + continue; + } + if !informative(&a.key_of(ga[0]).skeleton) { + summary.skeleton_groups_uninformative += 1; + continue; + } + for &ia in ga { + for &ib in gb { + let (ka, kb) = (a.key_of(ia), b.key_of(ib)); + let shape_match = ka.tier == KeyTier::Structural + && kb.tier == KeyTier::Structural + && ka.key == kb.key; + if same_name(ia, ib) || same_text(ia, ib) || shape_match { + continue; + } + let c = classify(&a.entries[ia], ka, &b.entries[ib], kb); + summary.candidates.add(Join::Skeleton, c); + emit(&record(a, ia, b, ib, Join::Skeleton, c, false)?)?; + } + } + } + + Ok(summary) +} + +/// Serialise `value` as one JCS line (RFC 8785 plus a final LF). +pub fn jcs_line(value: &T) -> Result> { + let mut bytes = serde_json_canonicalizer::to_vec(value)?; + bytes.push(b'\n'); + Ok(bytes) +} + +/// A whole scan: which pairs, where the corpora are, where output goes. +#[derive(Debug, Clone)] +pub struct RunOptions { + pub training_dir: PathBuf, + pub pairs: Vec<(String, String)>, + pub out: PathBuf, + pub scan: ScanOptions, + /// Collision groups to sample per corpus. + pub collision_samples: usize, +} + +/// What a run produced, for the CLI to print. Timings are reported here and +/// never written into the JCS files, which stay deterministic. +#[derive(Debug, Clone)] +pub struct RunReport { + pub coverage: Vec, + pub pairs: Vec, + pub load_times: Vec<(String, Duration)>, + pub pair_times: Vec<(String, Duration)>, + pub total: Duration, +} + +fn write_lines(path: &Path, items: &[T]) -> Result<()> { + let mut w = + BufWriter::new(File::create(path).with_context(|| format!("create {}", path.display()))?); + for item in items { + w.write_all(&jcs_line(item)?)?; + } + w.flush()?; + Ok(()) +} + +/// Load every corpus the pairs name (each once), scan each pair, and write +/// `pairs/__.jsonl`, `summary.jsonl`, `coverage.jsonl` and +/// `collisions/.jsonl` under `opts.out`. +/// +/// # Errors +/// +/// A corpus fails to load, or an output file cannot be written. +pub fn run(opts: &RunOptions) -> Result { + let started = Instant::now(); + if opts.pairs.is_empty() { + bail!("no corpus pairs to scan: pass --pair A:B or --preset"); + } + let needed: BTreeSet<&str> = opts + .pairs + .iter() + .flat_map(|(a, b)| [a.as_str(), b.as_str()]) + .collect(); + + let mut corpora: BTreeMap = BTreeMap::new(); + let mut load_times = Vec::new(); + for key in needed { + let t = Instant::now(); + let corpus = Corpus::load(&opts.training_dir, key)?; + load_times.push((key.to_string(), t.elapsed())); + corpora.insert(key.to_string(), corpus); + } + + let pairs_dir = opts.out.join("pairs"); + let collisions_dir = opts.out.join("collisions"); + fs::create_dir_all(&pairs_dir).with_context(|| format!("create {}", pairs_dir.display()))?; + fs::create_dir_all(&collisions_dir) + .with_context(|| format!("create {}", collisions_dir.display()))?; + + let coverage: Vec = corpora.values().map(Corpus::coverage).collect(); + write_lines(&opts.out.join("coverage.jsonl"), &coverage)?; + for c in corpora.values() { + write_lines( + &collisions_dir.join(format!("{}.jsonl", c.key)), + &c.collisions(opts.collision_samples), + )?; + } + + let mut summaries = Vec::new(); + let mut pair_times = Vec::new(); + for (ka, kb) in &opts.pairs { + let t = Instant::now(); + let path = pairs_dir.join(format!("{ka}__{kb}.jsonl")); + let mut w = BufWriter::new( + File::create(&path).with_context(|| format!("create {}", path.display()))?, + ); + let summary = scan_pair(&corpora[ka], &corpora[kb], &opts.scan, &mut |rec| { + w.write_all(&jcs_line(rec)?)?; + Ok(()) + })?; + w.flush()?; + pair_times.push((format!("{ka}:{kb}"), t.elapsed())); + summaries.push(summary); + } + write_lines(&opts.out.join("summary.jsonl"), &summaries)?; + + Ok(RunReport { + coverage, + pairs: summaries, + load_times, + pair_times, + total: started.elapsed(), + }) +} + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn folding_unifies_case_namespace_and_separator() { + assert_eq!(fold_name("nat.add_comm"), "add_comm"); + assert_eq!(fold_name("ADD_COMM"), "add_comm"); + assert_eq!(fold_name("add-comm"), "add_comm"); + assert_eq!(fold_name("Foo::bar"), "bar"); + assert_eq!(fold_name("_x_"), "x"); + } + + #[test] + fn generic_names_are_recognised() { + for g in [ + "lemma", + "lemma_3", + "lemma3", + "aux2", + "th27", + "ex1", + "z", + "anonymous", + "step2'", + ] { + assert!(is_generic(&fold_name(g)), "{g} should be generic"); + } + for n in ["add_comm", "append_assoc", "cos_add", "zip_unzip", "ext"] { + assert!(!is_generic(&fold_name(n)), "{n} should not be generic"); + } + } + + #[test] + fn presets_expand_as_documented() { + assert_eq!(preset_pairs("learning").unwrap().len(), 2); + assert_eq!(preset_pairs("spanning").unwrap().len(), 28); + assert_eq!(preset_pairs("in-family").unwrap().len(), 5); + assert_eq!(preset_pairs("full").unwrap().len(), 33); + assert!(preset_pairs("everything").is_none()); + } + + #[test] + fn pair_arguments_are_validated() { + assert_eq!( + parse_pair("hol4:hol_light").unwrap(), + ("hol4".to_string(), "hol_light".to_string()) + ); + assert!(parse_pair("hol4").is_err()); + assert!(parse_pair("hol4:hol4").is_err()); + assert!(parse_pair("../etc:hol4").is_err()); + } + + #[test] + fn similarity_ignores_variables_and_binders() { + assert_eq!( + similarity_permille("(EQ (ADD v0 v1) (ADD v1 v0))", "(EQ (ADD v2 v3) v4)"), + 1000 + ); + assert_eq!( + similarity_permille("(EQ (ADD v0 v1))", "(LE (MUL v0 v1))"), + 0 + ); + assert_eq!(similarity_permille("", ""), 0); + } + + #[test] + fn informative_rejects_variable_heads_and_bare_predicates() { + // `cos 0 = 1` and `n 0 = 1` under dk-shape-v1 + assert!(!informative("(EQ (v0 0) 1)")); + assert!(!informative("(EQ (v0 v1 v2) (v3 v1 v2))")); + assert!(!informative("(summable v0)")); + assert!(informative("(EQ (ADD v0 0) v0)")); + assert!(informative("(LT v0 (2 ^ v0))")); + assert!(informative( + "(EQ (MUL (MUL v0 v1) v2) (MUL v0 (MUL v1 v2)))" + )); + // `v10` in function position is still a variable head + assert!(!informative("(EQ (v10 0) (ADD 1 1))")); + // bare signatures: λProlog `int -> int -> int`, Dedukti `Int -> Int -> Int` + assert!(!informative("(ARROW INT (ARROW INT INT))")); + assert!(!informative("(ARROW (ARROW v0 v0) (ARROW v0 v0))")); + // ...and their skeletons, where sorts render as `?` + assert!(!informative("(ARROW ? (ARROW ? ?))")); + assert!(!informative("(ARROW ? ?)")); + assert!(informative("(ARROW (LE v0 v1) (LE (ADD v0 1) (ADD v1 1)))")); + } + + #[test] + fn pair_ids_ignore_side_order() { + let x = ("hol4", "ADD_COMM", "!m n. m + n = n + m"); + let y = ("hol_light", "ADD_SYM", "!m n. m + n = n + m"); + assert_eq!(pair_id(x, y).unwrap(), pair_id(y, x).unwrap()); + assert_ne!(pair_id(x, y).unwrap(), pair_id(x, x).unwrap()); + } +} diff --git a/src/rust/lib.rs b/src/rust/lib.rs index 3edf88d6..ec514d67 100644 --- a/src/rust/lib.rs +++ b/src/rust/lib.rs @@ -30,6 +30,7 @@ pub mod ids; // The single ID-minting module: UUIDv7 record ids, UUIDv8 content pub mod integrity; pub mod ipc; // L1: Cap'n Proto IPC transport (UDS primary, TCP fallback) pub mod learning; // Continuous self-learning loop (MCTS + self-play + curriculum + daemon) +pub mod lexicon; // Lexicon candidate mining across corpora (echidna lexicon scan) pub mod llm; // Frontier LLM advisor (via BoJ Server) pub mod neural; pub mod parsers; diff --git a/src/rust/main.rs b/src/rust/main.rs index 60f9616d..73c3857a 100644 --- a/src/rust/main.rs +++ b/src/rust/main.rs @@ -196,6 +196,12 @@ enum Commands { op: CorpusOp, }, + /// Mine lexicon candidates across training corpora (flag-only) + Lexicon { + #[command(subcommand)] + op: LexiconOp, + }, + /// Search proof-design space via simulated annealing Design { #[command(subcommand)] @@ -361,6 +367,39 @@ enum CorpusOp { }, } +#[derive(Subcommand)] +enum LexiconOp { + /// Pair theorem names and canonical statement shapes across training + /// corpora and write review candidates as JCS JSON Lines. Every + /// candidate carries `evidence = none`; `data/synonyms/` is never edited. + Scan { + /// Directory holding `proof_states_.jsonl` files. + #[arg(long, default_value = "training_data")] + training_dir: PathBuf, + /// A corpus pair, `A:B`. Repeatable; combines with `--preset`. + #[arg(long = "pair", value_name = "A:B")] + pairs: Vec, + /// A named pair set: `learning`, `spanning`, `in-family` or `full`. + #[arg(long)] + preset: Option, + /// Output directory (pairs/, collisions/, summary.jsonl, coverage.jsonl). + #[arg(long, default_value = "target/lexicon-scan")] + out: PathBuf, + /// Also emit pairs whose shared name is generic (`lemma3`, `aux`, `ex1`). + #[arg(long)] + keep_generic: bool, + /// Skip a shared name whose statement cross product exceeds this. + #[arg(long, default_value_t = 64)] + max_pairs_per_name: usize, + /// Skip a shape or skeleton group larger than this on either side. + #[arg(long, default_value_t = 8)] + max_shape_group: usize, + /// Key-collision groups to sample per corpus. + #[arg(long, default_value_t = 40)] + collision_samples: usize, + }, +} + #[derive(Subcommand)] enum DesignOp { /// Run SA over a named design problem. @@ -541,6 +580,10 @@ async fn main() -> Result<()> { corpus_command(op, &formatter)?; }, + Commands::Lexicon { op } => { + lexicon_command(op)?; + }, + Commands::Design { op } => { design_command(op, &formatter).await?; }, @@ -1324,6 +1367,129 @@ async fn diagnostics_command() -> Result<()> { Ok(()) } +/// Lexicon command - mine cross-corpus candidates for curation. +/// +/// The scan runs on a thread with a large stack: the canonicaliser's parser +/// recurses on nesting depth, and some corpus statements (ACL2 books) nest +/// deeply. Timings go to stderr; the JCS files under `--out` carry none, so +/// two runs over the same data write the same bytes. +/// +/// # Errors +/// +/// An unknown preset, a malformed `--pair`, no pairs at all, a corpus that +/// fails to load, or an output file that cannot be written. +fn lexicon_command(op: LexiconOp) -> Result<()> { + use echidna::lexicon::scan::{self, RunOptions, ScanOptions}; + + let LexiconOp::Scan { + training_dir, + pairs, + preset, + out, + keep_generic, + max_pairs_per_name, + max_shape_group, + collision_samples, + } = op; + + let mut all_pairs = Vec::new(); + if let Some(name) = preset.as_deref() { + all_pairs.extend(scan::preset_pairs(name).with_context(|| { + format!("unknown preset `{name}` (learning, spanning, in-family, full)") + })?); + } + for p in &pairs { + let pair = scan::parse_pair(p)?; + if !all_pairs.contains(&pair) { + all_pairs.push(pair); + } + } + let opts = RunOptions { + training_dir, + pairs: all_pairs, + out, + scan: ScanOptions { + keep_generic, + max_pairs_per_name, + max_shape_group, + }, + collision_samples, + }; + + let report = std::thread::Builder::new() + .name("lexicon-scan".into()) + .stack_size(512 * 1024 * 1024) + .spawn(move || scan::run(&opts).map(|r| (r, opts.out))) + .context("spawn the scan thread")? + .join() + .map_err(|_| anyhow::anyhow!("the scan thread panicked"))??; + let (report, out) = report; + + println!( + "{:<14} {:>8} {:>8} {:>6} {:>7} {:>6} {:>6} {:>6} {:>8}", + "corpus", "rows", "names", "hom%", "struct%", "skel%", "text%", "cmpl%", "collide" + ); + for c in &report.coverage { + let pct = |n: usize| 100.0 * n as f64 / c.rows.max(1) as f64; + println!( + "{:<14} {:>8} {:>8} {:>6.1} {:>7.1} {:>6.1} {:>6.1} {:>6.1} {:>8}", + c.corpus, + c.rows, + c.names, + 100.0 * c.homonym_names as f64 / c.names.max(1) as f64, + pct(c.tiers.structural), + pct(c.tiers.skeleton), + pct(c.tiers.text), + pct(c.tiers.complete), + c.collision_keys + ); + } + println!(); + println!( + "{:<26} {:>7} {:>7} {:>7} {:>7} {:>7} {:>7} {:>7} {:>8} {:>7} {:>7} {:>7}", + "pair", + "shared", + "generic", + "capped", + "exact", + "shape", + "skel", + "differs", + "unparsed", + "syn-tx", + "syn-sh", + "syn-sk" + ); + for s in &report.pairs { + let names = [&s.candidates.name_exact, &s.candidates.name_folded]; + let sum = + |f: fn(&scan::CandidateCounts) -> usize| names.iter().map(|c| f(c)).sum::(); + println!( + "{:<26} {:>7} {:>7} {:>7} {:>7} {:>7} {:>7} {:>7} {:>8} {:>7} {:>7} {:>7}", + format!("{}:{}", s.pair[0], s.pair[1]), + s.folded_names_shared, + s.generic_names_skipped, + s.name_pairs_capped, + sum(|c| c.cognate_exact), + sum(|c| c.cognate_shape), + sum(|c| c.cognate_skeleton), + sum(|c| c.differs), + sum(|c| c.unparsed), + s.candidates.text.total(), + s.candidates.shape.total(), + s.candidates.skeleton.total() + ); + } + for (corpus, t) in &report.load_times { + eprintln!("load {corpus}: {:.2?}", t); + } + for (pair, t) in &report.pair_times { + eprintln!("scan {pair}: {:.2?}", t); + } + eprintln!("total: {:.2?}; output in {}", report.total, out.display()); + Ok(()) +} + /// Corpus command - ingest, query, or summarise a project corpus. /// /// First adapter is `agda`, targeted at echo-types' Buchholz / Brouwer diff --git a/tests/lexicon_fixtures/scan/proof_states_hol4_mini.jsonl b/tests/lexicon_fixtures/scan/proof_states_hol4_mini.jsonl new file mode 100644 index 00000000..971c31f0 --- /dev/null +++ b/tests/lexicon_fixtures/scan/proof_states_hol4_mini.jsonl @@ -0,0 +1,6 @@ +{"goal":"!m n. m + n = n + m","theorem":"ADD_SYM"} +{"goal":"!x y d. 0 < d /\\ ((x - d) < y) /\\ (y < (x + d)) <=> abs(y - x) < d","theorem":"ABS_BETWEEN"} +{"goal":"FACT 0 = 1","theorem":"FACT_0"} +{"goal":"T","theorem":"lemma"} +{"goal":"F ==> T","theorem":"lemma"} +{"goal":"0 + n = n","theorem":"ADD_0"} diff --git a/tests/lexicon_fixtures/scan/proof_states_hol_light_mini.jsonl b/tests/lexicon_fixtures/scan/proof_states_hol_light_mini.jsonl new file mode 100644 index 00000000..58c332cb --- /dev/null +++ b/tests/lexicon_fixtures/scan/proof_states_hol_light_mini.jsonl @@ -0,0 +1,5 @@ +{"goal":"!m n. m + n = n + m","theorem":"ADD_SYM"} +{"goal":"!x y d. &0 < d /\\ ((x - d) < y) /\\ (y < (x + d)) <=> abs(y - x) < d","theorem":"ABS_BETWEEN"} +{"goal":"FACT 0 = 1","theorem":"FACT"} +{"goal":"~F","theorem":"lemma"} +{"goal":"0 + n = n","theorem":"ADD_0"} diff --git a/tests/lexicon_fixtures/scan/proof_states_isabelle_mini.jsonl b/tests/lexicon_fixtures/scan/proof_states_isabelle_mini.jsonl new file mode 100644 index 00000000..bb9a251a --- /dev/null +++ b/tests/lexicon_fixtures/scan/proof_states_isabelle_mini.jsonl @@ -0,0 +1,8 @@ +{"goal":"(a b : nat) : a + b = b + a","theorem":"add_comm"} +{"goal":"(p q : nat) : p * q = q * p","theorem":"MUL_COMM"} +{"goal":"(n : int) : n + 0 = n","theorem":"add_zero"} +{"goal":"(x : nat) : 0 ^ x = 0","theorem":"pow_zero"} +{"goal":"(x y z : nat) : x * y * z = x * (y * z)","theorem":"times_assoc"} +{"goal":": exp 0 = 1","theorem":"exp_zero"} +{"goal":"(u v : nat) : u = v","theorem":"ext"} +{"goal":"(u v : int) : u * u = v","theorem":"ext"} diff --git a/tests/lexicon_fixtures/scan/proof_states_lean_mini.jsonl b/tests/lexicon_fixtures/scan/proof_states_lean_mini.jsonl new file mode 100644 index 00000000..8a61fad0 --- /dev/null +++ b/tests/lexicon_fixtures/scan/proof_states_lean_mini.jsonl @@ -0,0 +1,9 @@ +{"goal":"(x y : nat) : x + y = y + x","theorem":"add_comm"} +{"goal":"(m n : nat) : m * n = n * m","theorem":"nat.mul_comm"} +{"goal":"(n : nat) : n + 0 = n","theorem":"add_zero"} +{"goal":"(x : nat) : x ^ 0 = 1","theorem":"pow_zero"} +{"goal":"(a b c : nat) : a * b * c = a * (b * c)","theorem":"mul_assoc"} +{"goal":": cos 0 = 1","theorem":"cos_zero"} +{"goal":"(a b : nat) : a = b","theorem":"ext"} +{"goal":"(a b : int) : a + 0 = b","theorem":"ext"} +{"goal":"(p q : nat) : p * 1 = q","theorem":"ext"} diff --git a/tests/lexicon_scan_test.rs b/tests/lexicon_scan_test.rs new file mode 100644 index 00000000..5acc03b5 --- /dev/null +++ b/tests/lexicon_scan_test.rs @@ -0,0 +1,201 @@ +// SPDX-License-Identifier: MPL-2.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) + +//! `echidna lexicon scan` over small fixture corpora +//! (`tests/lexicon_fixtures/scan/proof_states_*.jsonl`). +//! +//! The HOL fixtures are real rows from `training_data/` for the stage-6a +//! pilot pair. `dk-shape-v1` cannot read HOL notation, so the scan must say +//! so (`unparsed`) rather than invent shape matches. The `lean_mini` / +//! `isabelle_mini` fixtures use syntax the scheme reads completely, so every +//! join and classification can be pinned there. + +use std::collections::BTreeSet; +use std::path::{Path, PathBuf}; + +use echidna::lexicon::scan::{ + self, Candidate, CandidateRecord, Corpus, Join, PairSummary, RunOptions, ScanOptions, +}; + +fn fixtures() -> PathBuf { + Path::new(env!("CARGO_MANIFEST_DIR")).join("tests/lexicon_fixtures/scan") +} + +fn load(key: &str) -> Corpus { + Corpus::load(&fixtures(), key).unwrap_or_else(|e| panic!("{key}: {e:#}")) +} + +fn scan(a: &str, b: &str, opts: &ScanOptions) -> (PairSummary, Vec) { + let (ca, cb) = (load(a), load(b)); + let mut out = Vec::new(); + let summary = scan::scan_pair(&ca, &cb, opts, &mut |r| { + out.push(r.clone()); + Ok(()) + }) + .expect("scan"); + (summary, out) +} + +fn find<'r>(records: &'r [CandidateRecord], a: &str, b: &str) -> &'r CandidateRecord { + records + .iter() + .find(|r| r.a.name == a && r.b.name == b) + .unwrap_or_else(|| panic!("no record for {a} ~ {b}")) +} + +#[test] +fn hol_pilot_pair_is_classified_honestly() { + let (summary, records) = scan("hol4_mini", "hol_light_mini", &ScanOptions::default()); + + // Identical text is a cognate whatever the canonicaliser makes of it. + assert_eq!( + find(&records, "ADD_SYM", "ADD_SYM").candidate, + Candidate::CognateExact + ); + assert_eq!( + find(&records, "ADD_0", "ADD_0").candidate, + Candidate::CognateExact + ); + + // `0 < d` against `&0 < d`: the HOL Light statement is over the reals. + // dk-shape-v1 cannot read `!` binders, so neither side is complete and + // the pair is `unparsed`, not a shape cognate and not `differs`. + let abs = find(&records, "ABS_BETWEEN", "ABS_BETWEEN"); + assert_eq!(abs.candidate, Candidate::Unparsed); + assert!(!abs.a.complete && !abs.b.complete); + + // Different names, identical text: found by the text join although the + // canonicaliser drops HOL's `FACT` as a declaration keyword. + let fact = find(&records, "FACT_0", "FACT"); + assert_eq!(fact.join, Join::Text); + assert_eq!(fact.candidate, Candidate::CognateExact); + + // `lemma` is shared but generic. + assert_eq!(summary.generic_names_skipped, 1); + assert!(!records.iter().any(|r| r.a.name == "lemma")); + + // Nothing in this pair parses completely, so no shape or skeleton join. + assert_eq!(summary.candidates.shape.total(), 0); + assert_eq!(summary.candidates.skeleton.total(), 0); +} + +#[test] +fn every_join_and_class_on_complete_syntax() { + let (summary, records) = scan("lean_mini", "isabelle_mini", &ScanOptions::default()); + + // Same name, alpha-variants. + let add_comm = find(&records, "add_comm", "add_comm"); + assert_eq!(add_comm.join, Join::NameExact); + assert_eq!(add_comm.candidate, Candidate::CognateShape); + + // Names equal only after folding (`nat.mul_comm` / `MUL_COMM`). + let mul_comm = find(&records, "nat.mul_comm", "MUL_COMM"); + assert_eq!(mul_comm.join, Join::NameFolded); + assert_eq!(mul_comm.candidate, Candidate::CognateShape); + + // `nat` against `int`: the skeletons agree, the shapes do not. + let add_zero = find(&records, "add_zero", "add_zero"); + assert_eq!(add_zero.candidate, Candidate::CognateSkeleton); + + // Same name, different statement: a false-friend candidate. + assert_eq!( + find(&records, "pow_zero", "pow_zero").candidate, + Candidate::Differs + ); + + // Different names, the same shape: a synonym candidate. + let assoc = find(&records, "mul_assoc", "times_assoc"); + assert_eq!(assoc.join, Join::Shape); + assert_eq!(assoc.candidate, Candidate::CognateShape); + + // `cos 0 = 1` and `exp 0 = 1` share a dk-shape-v1 key (`cos`/`exp` are + // renamed as variables); the join refuses it as uninformative. + assert!(!records.iter().any(|r| r.a.name == "cos_zero")); + assert!(summary.shape_groups_uninformative >= 1); + + // Homonyms: `ext` has 3 Lean and 2 Isabelle statements, 6 pairs. + let ext = records.iter().filter(|r| r.a.name == "ext").count(); + assert_eq!(ext, 6); + + // Every record is flag-only. + for r in &records { + assert_eq!( + serde_json::to_value(&r.evidence).unwrap(), + serde_json::json!({"kind": "none"}) + ); + } +} + +#[test] +fn homonym_cross_products_over_the_cap_are_counted_not_emitted() { + let opts = ScanOptions { + max_pairs_per_name: 4, + ..ScanOptions::default() + }; + let (summary, records) = scan("lean_mini", "isabelle_mini", &opts); + assert!(!records.iter().any(|r| r.a.name == "ext")); + assert_eq!(summary.name_pairs_capped, 1); + assert_eq!(summary.statement_pairs_capped, 6); +} + +#[test] +fn records_are_jcs_and_ids_ignore_scan_direction() { + let (_, forward) = scan("lean_mini", "isabelle_mini", &ScanOptions::default()); + let (_, backward) = scan("isabelle_mini", "lean_mini", &ScanOptions::default()); + + for r in &forward { + let line = scan::jcs_line(r).unwrap(); + assert_eq!(*line.last().unwrap(), b'\n'); + let body = &line[..line.len() - 1]; + let reparsed: serde_json::Value = serde_json::from_slice(body).unwrap(); + assert_eq!(serde_json_canonicalizer::to_vec(&reparsed).unwrap(), body); + assert_eq!(uuid::Uuid::parse_str(&r.id).unwrap().get_version_num(), 8); + } + + let ids = |rs: &[CandidateRecord]| rs.iter().map(|r| r.id.clone()).collect::>(); + assert_eq!(ids(&forward), ids(&backward)); + assert_eq!(ids(&forward).len(), forward.len(), "ids are unique"); +} + +#[test] +fn a_run_writes_the_same_bytes_twice() { + let base = std::env::temp_dir().join(format!("echidna-lexicon-scan-{}", std::process::id())); + let run_into = |dir: &str| { + let out = base.join(dir); + let report = scan::run(&RunOptions { + training_dir: fixtures(), + pairs: vec![ + ("lean_mini".into(), "isabelle_mini".into()), + ("hol4_mini".into(), "hol_light_mini".into()), + ], + out: out.clone(), + scan: ScanOptions::default(), + collision_samples: 10, + }) + .expect("run"); + assert_eq!(report.pairs.len(), 2); + assert_eq!(report.coverage.len(), 4); + out + }; + let (one, two) = (run_into("one"), run_into("two")); + for file in [ + "summary.jsonl", + "coverage.jsonl", + "pairs/lean_mini__isabelle_mini.jsonl", + "pairs/hol4_mini__hol_light_mini.jsonl", + "collisions/lean_mini.jsonl", + ] { + let (x, y) = ( + std::fs::read(one.join(file)).unwrap(), + std::fs::read(two.join(file)).unwrap(), + ); + assert_eq!(x, y, "{file} differs between runs"); + } + let _ = std::fs::remove_dir_all(&base); +} + +#[test] +fn unknown_corpus_keys_fail_loudly() { + assert!(Corpus::load(&fixtures(), "no_such_corpus").is_err()); + assert!(Corpus::load(&fixtures(), "../etc").is_err()); +} From 898912aa66eb7ebec1d01e5be3b7792d3e542b49 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 27 Oct 2026 04:22:15 +0000 Subject: [PATCH 04/16] docs(lexicon): PR 3 results, dk-shape-v1 limits, invariant/witness reading Records what the scan measured over thirteen training_data/ corpora: how much dk-shape-v1 reads completely (0.3 % to 94 %), the four rule-level causes of false identity left for a dk-shape-v2 decision (D6), the data problems in the ACL2 and ACL2s extractors (D7), and the cross-family synonym candidates that held up. Adds the knot-theory reading of equivalence (invariants against witnesses; difference is cheap only from a semantic invariant), why the scan emits JCS and not TOML, and the ruling that phrase detection follows this PR. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01WS4mfQeC3N1DWjcCQJaQqw --- CHANGELOG.adoc | 27 +++ ...9-lexicon-v2-and-identity-arbitration.adoc | 192 +++++++++++++++++- 2 files changed, 217 insertions(+), 2 deletions(-) diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index d34ce627..d31ef171 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -8,6 +8,33 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning]. === [Unreleased] +==== Added — `echidna lexicon scan`, 2026-10-27 + +* *`+echidna lexicon scan+`* (`+src/rust/lexicon/scan.rs+`, + `+just lexicon-scan+`) — compares `+training_data/+` corpora by theorem + name and by canonical statement shape, and writes cognates, false-friend + and specialisation candidates, and synonym candidates (joined by + identical text, shape or skeleton) as JCS JSON Lines with UUIDv8 pair + ids. Flag-only: every record carries `+evidence = none+`, and + `+data/synonyms/+` is never written. Presets `+learning+`, + `+spanning+` (one corpus per prover family), `+in-family+` and `+full+`. + Per-corpus coverage and key-collision samples are written alongside. + +==== Fixed — canonicaliser, 2026-10-27 + +* *`+corpus::canonical+` no longer panics* on a statement whose last + token is an unbalanced opening bracket (eight `+open + 1..close+` slices + are now guarded). `+structural_key+` reaches this from `+corpus ingest+` + and the octad identity keys. No key changes. +* *`+StructuralKey::complete+`* (new, `+#[serde(default)]+`) reports + whether the shape accounts for the whole statement: false when the + parser stops early, meets notation `+dk-shape-v1+` has no rule for + (HOL binders, Isabelle `+\<…>+` escapes), drops a statement's own leading + tokens as a "header", or misreads a leading group as a telescope. No key + changes. Measured on `+training_data/+`, 0.3 %–94 % of a corpus is read + completely; the rule-level causes are recorded for a `+dk-shape-v2+` + decision in `+docs/decisions/2026-10-19-lexicon-v2-and-identity-arbitration.adoc+`. + ==== Added — structural cross-prover identity keys, 2026-10-22 * *`+src/rust/corpus/canonical.rs+`* — normalises a declaration's *type* diff --git a/docs/decisions/2026-10-19-lexicon-v2-and-identity-arbitration.adoc b/docs/decisions/2026-10-19-lexicon-v2-and-identity-arbitration.adoc index 30b4c41b..cc1b3399 100644 --- a/docs/decisions/2026-10-19-lexicon-v2-and-identity-arbitration.adoc +++ b/docs/decisions/2026-10-19-lexicon-v2-and-identity-arbitration.adoc @@ -2,7 +2,7 @@ // SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) = ADR: lexicon v2 (false friends, phrases, equivalences) and hub-and-probe identity arbitration (stage 6c) :revdate: 2026-10-19 -:status: accepted in part — D1, D2 and D4 ruled 2026-10-19 (§7); D3 and D5 open +:status: accepted in part — D1, D2 and D4 ruled 2026-10-19 (§7); D3, D5, D6 and D7 open == Context (measured on `main` at `ed6ef60`, 2026-10-19) @@ -294,11 +294,197 @@ re-running `metrics/run_all.jl` to re-baseline `oov_rate` and verdict's `level` should surface in its trust bridge once dispatch attaches evidence. +== PR 3 results: `echidna lexicon scan` (2026-10-27) + +=== What landed + +`echidna lexicon scan` (`src/rust/lexicon/scan.rs`, `just lexicon-scan`) +compares `training_data/proof_states_.jsonl` corpora on two axes: +the theorem *name*, and the canonical *shape* of its statement. Same name +and same shape is a cognate; same name and a different shape is a false +friend or a specialisation; a different name and the same shape (or +identical text, or the same skeleton) is a synonym candidate. Output is +I-JSON serialised as JCS, one record per line, with a UUIDv8 content id per +statement pair that does not depend on scan direction or normaliser +version, so a review decision survives a re-scan. Every candidate carries +`evidence = { kind = "none" }` and nothing is written to `data/synonyms/` +(D4). The pair sets follow the 2026-10-20 ruling: a learning pass +(HOL4 ↔ HOL Light, Lean 3 ↔ AFP), then one corpus per family +(HOL4, AFP, Lean 3, Mizar, ACL2, Why3, λProlog, Dedukti: 28 pairs) plus one +pair inside each family (5 more). + +=== A departure, labelled + +The 2026-10-20 ruling was a lexical normaliser in this PR and parsed +normalisation in PR 6. Before this PR was written, #449 landed +`src/rust/corpus/canonical.rs` (`dk-shape-v1`), a canonicaliser that +already does the lexical part and more. Building a second one beside it +would have been a parallel normaliser; the scan uses `dk-shape-v1` instead +and measures it. That is the departure, and the measurement is why it paid. + +=== What the measurement found in `dk-shape-v1` + +The scan's first run panicked inside `canonical.rs`: an unbalanced opening +bracket as the last token made eight `open + 1..close` slices panic. That +path is also `corpus ingest`'s. Fixed here with no key change (reproduced +first; the regression test panics on the old code). + +The second finding is larger. When the canonicaliser cannot read a +statement it rarely falls back to its text tier; it returns a +*structural-tier* key for the prefix it did read, and different statements +share that prefix. `StructuralKey::complete` now says whether the whole +statement was read. It is false when the parser stops early, when the body +holds notation the scheme has no rule for (`!`, `?`, `@` and `\` binders, +Isabelle's `\<…>` escapes, Lean 3's `$`), when a header drop discarded +the statement's own tokens, or when a leading bracket group was misread as +a binder telescope. It changes no key. The scan treats an +incomplete key as no identity: such pairs are `unparsed`, and such +statements take no part in shape joins. + +Share of each corpus read completely (`dk-shape-v1`, 2026-10-27): + +[cols="2,2,2,2,2",options="header"] +|=== +| Corpus | Distinct rows | Read completely | Keys shared by distinct statements | Homonymous names +| acl2 | 135963 | 25.6 % | 2063 | 7.9 % +| acl2s | 112677 | 88.1 % | 3576 | 4.7 % +| afp | 102683 | 10.8 % | 530 | 2.0 % +| agda | 46028 | 41.4 % | 585 | 8.6 % +| dafny | 10487 | 58.4 % | 202 | 12.1 % +| dedukti | 1453 | 77.4 % | 57 | 20.6 % +| hol4 | 95738 | 10.0 % | 130 | 4.1 % +| hol_light | 43937 | 2.5 % | 24 | 2.8 % +| isabelle_zf | 3577 | 0.3 % | 0 | 0.3 % +| lambda_prolog | 24897 | 94.0 % | 133 | 49.9 % +| lean3 | 92680 | 27.3 % | 2901 | 19.1 % +| mizar | 76522 | 20.5 % | 512 | 1.8 % +| why3 | 25180 | 30.5 % | 396 | 21.8 % +|=== + +"Keys shared by distinct statements" counts complete keys only. Most are +benign (Lean 3 goal fields sometimes repeat the statement with its proof +attached, which the canonicaliser cuts); the rest are the rule-level +causes below. + +Four rule-level causes of false identity cannot be fixed without changing +keys, so they are recorded here for a `dk-shape-v2` decision (D6) rather +than changed under `dk-shape-v1`: + +. *Header drop.* `drop_declared_head` is documented to skip a group that + *starts* the statement, but returns at the first top-level bracket + anywhere. A statement with no `name :` header loses everything before + its first bracket: `exp(0) = 1` and `cos(0) = 1` both key as + `(EQ 0 1)`; `closed (closure M)` keys as `(closure v0)`. +. *Keyword drop.* Declaration keywords match case-insensitively at the + start of any statement: HOL4's `FACT 1 = 1` keys as `1 = 1`. +. *Short names as variables.* Any lower-case name of three characters or + fewer is numbered as a variable, so `cos`, `exp`, `nhd`, `phi` vanish: + `nhd 0 = 0` and `phi 0 = 0` share a key. +. *Unread notation and binders.* No HOL (`!`, `?`, `\`, `==>`, `~`) or + Isabelle `\<…>` notation. No ∃: `exists x : nat, x = 0` and + `exists x : nat, x = 1` both key as `NAT`. A parenthesised quantified + antecedent at the start is read as a binder telescope: + `(forall x : nat, P x) -> Q` keys as `(PI [NAT NAT] v0)`, with `forall` + taken as a bound name. A Lean hypothesis binder `(h : 2 * n ≤ n)` is + reduced to a sort, so `(h : 2 * n ≤ n) : n = 0` and + `(h : n ≤ n / 2) : n = 0` share a key. Binder keywords elsewhere are + lifted into the leading Π (`extract_binders` step 3), which is sound only + in positive positions; the probes found no pair merged by that alone. + +`complete` now flags the header drop, the keyword drop, unread notation, +∃ (the parser stops) and the telescope misread. It does not flag the +short-name rule or the hypothesis-as-sort rule, which produce well-formed +but wrong shapes; the scan's `informative` filter catches the short-name +rule's commonest form (a variable in function position). The corpus +identity keys (E6 `cross_prover_identity_key`) inherit all four causes. + +=== What the measurement found in the corpora + +Over all 33 pairs: 203,860 same-name statement pairs, of which 1,070 are +exact cognates, 3,619 shape cognates, 76 skeleton (specialisation) +candidates, 36,470 differ, and 162,625 (80 %) are `unparsed`. Synonym +candidates under different names: 269 by identical text, 848 by shape, +882 by skeleton. Debug build: 171 s for all thirteen corpora, almost all +of it loading and canonicalising; one pair scans in about a second. + +* *HOL4 ↔ HOL Light* (pilot pair): 1,033 exact cognates and 144 text + synonyms (`FACT_0` / `pth_0`), but 5,550 same-name pairs `unparsed`: + `dk-shape-v1` reads 2.5 % of HOL Light. The pilot pair needs HOL + notation in the canonicaliser before shape evidence means anything. +* *Lean 3 ↔ AFP, AFP ↔ Mizar, Lean 3 ↔ Mizar*: the synonym joins find real + cross-family correspondences: `sqrt_zero ~ lemSqrt0`, + `dist_comm ~ dist_sym`, `add_comm ~ plus_commute`, + `cantor ~ x_lt_2_x` (`a < 2^a` over cardinals and naturals), + `lt_add_one_iff ~ Th13`, and Mizar's article-local labels (`Th29`) + matched by content to named AFP and Lean lemmas. +* *ACL2 and ACL2s are dirty at the source*: ACL2s goals are truncated + mid-expression or are comments (`;; (implies …`), and ACL2 goals carry + `:hints` text and terminal escape codes. 95,651 shared names yield 31 + exact cognates. The extractors need fixing (D7). +* *Thin shapes are not synonyms*: a variable in function position (the + short-name rule above), fewer than three constants, or a bare type + signature (λProlog's `int -> int -> int` against Dedukti's + `Int -> Int -> Int`) say nothing about which statement it is. Joins + between different names skip them (3,749 groups, counted). + +=== Equivalence by invariant and by witness + +Knot theory decides the same question echidna faces. Two knots are equal +when one deforms into the other; in practice that is settled two ways. An +*invariant* (the Jones polynomial, quandle colourings) is cheap and can +prove two knots *different*, but agreement proves sameness only if the +invariant is complete. A *witness* (a sequence of Reidemeister moves) is +expensive and proves sameness, step by checkable step. The knot quandle is +complete up to an orientation symmetry (Joyce; Matveev, 1982), which is +why QuandleDB (`nextgen-databases/quandledb`) is built on it. + +Echidna's evidence ladder has the same two halves. Canonical keys and +consequence probes are invariants: agreement is a candidate (`belief`) or +`epi`, never `sound`. A kernel-checked translation is the witness: `sound`. +Three consequences follow. + +. *Difference is cheaper than sameness, but only from a semantic + invariant.* One verified consequence that holds of one statement and + fails of the other, read in one shared standpoint, is a sound + certificate of *distinctness*: a false friend can be proved, not just + suspected. PR 4's probe loop should report `distinct` as a first-class + outcome. A *syntactic* key that differs proves nothing: this PR shows + normalisation gaps separate equal statements and merge different ones. +. *A complete invariant is as good as a witness.* PR 6's injectivity + property test (distinct terms in the fragment never share a `term_hash`) + is exactly a completeness proof for the λΠ projection on its fragment. + `dk-shape-v1` is far from complete, and the table above says how far. +. *The residue of a lossy correspondence* (`fidelity = lossy`) is what the + invariant cannot see; echo-types' loss-with-residue formalism is the + vocabulary for it, as §3 already cites. + +=== Formats: why the scan emits JCS and not TOML + +TOML has no canonical form: the same data has many valid spellings +(inline or standard tables, dotted keys, four string styles, several float +and date forms), and no specification fixes one. So TOML cannot be hashed +or diffed stably, and it carries types I-JSON lacks (datetimes, 64-bit +integers beyond I-JSON's safe range). Machine output is therefore JCS. The +curated tables stay TOML for people (D2); if a table needs a content id, +the id of record is the JCS of its *parsed* data, which gives TOML a +canonical identity without changing how it is written. + +=== Ordering + +Phrase detection (an extractor that finds multi-token idioms at proof +sites, so the canonical spelling of a `phrase` row can be replaced as well +as its aliases) comes after this PR, by the 2026-10-20 ruling. + == Owner decisions Ruled 2026-10-19 through the selector: D1, D2 and D4. D3 and D5 remain open. The owner also ruled the pacing: PRs 1 and 3 proceed now; PRs 4–6 (arbiter -and ABI changes, kernel translation) wait for the stronger model. +and ABI changes, kernel translation) wait for the stronger model. Ruled +2026-10-20: the PR 3 normaliser is lexical with parsed normalisation in +PR 6 (superseded in practice by #449's canonicaliser, see PR 3 results), +the scan covers one corpus per family plus one in-family pair each, its +records carry UUIDv8 ids, the invariant/witness reading goes in this ADR, +and phrase detection follows PR 3. D6 and D7 opened 2026-10-27. [cols="1,5,3,3",options="header"] |=== @@ -308,6 +494,8 @@ and ABI changes, kernel translation) wait for the stronger model. | D3 | First consequence-probe pair: Z3 ↔ CVC5 (runs in CI today) alongside the HOL4 ↔ HOL Light hub pilot, or wait for HOL binaries in CI? | Z3 ↔ CVC5 now | open | D4 | May corpus-mined candidates set `semantic_class` automatically? | No: `evidence = none`, flag-only until curated or probe-tested | as recommended | D5 | Open the verisimdb consonance-subject issue (option E) now? | Yes | open +| D6 | Fix `dk-shape-v1`'s four rule-level false-identity causes (header drop, keyword drop, short names as variables, unread notation and binders) as `dk-shape-v2`, bumping `SCHEME` and so every corpus identity key? | Yes, as its own PR, starting with the header and keyword drops (smallest, largest effect), with the scan as the before/after measure | open +| D7 | Fix the `training_data/` extractors for ACL2 (hints, escape codes) and ACL2s (truncation, comment lines), and strip proof bodies from Lean 3 goals? | Yes, at the extractors, then re-scan | open |=== == Non-claims From 3a390c02be2c9df8d339b3c782dadb65d8e2f100 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 27 Oct 2026 04:49:23 +0000 Subject: [PATCH 05/16] fix(lexicon): complete catches truncation and HOL ~/==>; scan output is unambiguous Addresses the Codex review of #453. - `StructuralKey::complete` is false when the input ends inside an open bracket (`(x = y`): the parser reached the end with the group open and the flag said complete. ACL2s goals truncated mid-expression are exactly this, and were entering shape joins. Measured effect: ACL2s read completely falls from 88 % to 5 %, and `differs` across all 33 pairs from 36,470 to 8,414, most of those now `unparsed`. - HOL's `~` and `==>` count as unread notation. `==>` lexes as `==` `>`; the flag looks for that token pair so the lexer, and every key, stay as they were. - A corpus key may not contain `__`, so `pairs/__.jsonl` names one pair only. - `--pair b:a` is the same pair as a preset's `a:b` and is scanned once. - A run removes the previous run's `.jsonl` files from `pairs/` and `collisions/` before writing, so a smaller re-run leaves no stale candidates beside its summary. Nothing else in the directory is touched. Tests cover each case; the ADR and CHANGELOG carry the re-measured numbers. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_01WS4mfQeC3N1DWjcCQJaQqw --- CHANGELOG.adoc | 9 +-- ...9-lexicon-v2-and-identity-arbitration.adoc | 55 +++++++++--------- src/rust/corpus/canonical.rs | 56 +++++++++++++++---- src/rust/lexicon/scan.rs | 17 ++++++ src/rust/main.rs | 7 ++- tests/lexicon_scan_test.rs | 34 +++++++++++ 6 files changed, 136 insertions(+), 42 deletions(-) diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index d31ef171..79e78c71 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -28,10 +28,11 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning]. and the octad identity keys. No key changes. * *`+StructuralKey::complete+`* (new, `+#[serde(default)]+`) reports whether the shape accounts for the whole statement: false when the - parser stops early, meets notation `+dk-shape-v1+` has no rule for - (HOL binders, Isabelle `+\<…>+` escapes), drops a statement's own leading - tokens as a "header", or misreads a leading group as a telescope. No key - changes. Measured on `+training_data/+`, 0.3 %–94 % of a corpus is read + parser stops early or the input ends inside an open bracket, meets + notation `+dk-shape-v1+` has no rule for (HOL binders, `+~+`, `+==>+`, + Isabelle `+\<…>+` escapes), drops a statement's own leading tokens as a + "header", or misreads a leading group as a telescope. No key changes. + Measured on `+training_data/+`, 0.4 %–94 % of a corpus is read completely; the rule-level causes are recorded for a `+dk-shape-v2+` decision in `+docs/decisions/2026-10-19-lexicon-v2-and-identity-arbitration.adoc+`. diff --git a/docs/decisions/2026-10-19-lexicon-v2-and-identity-arbitration.adoc b/docs/decisions/2026-10-19-lexicon-v2-and-identity-arbitration.adoc index cc1b3399..73b4d5e3 100644 --- a/docs/decisions/2026-10-19-lexicon-v2-and-identity-arbitration.adoc +++ b/docs/decisions/2026-10-19-lexicon-v2-and-identity-arbitration.adoc @@ -333,11 +333,13 @@ The second finding is larger. When the canonicaliser cannot read a statement it rarely falls back to its text tier; it returns a *structural-tier* key for the prefix it did read, and different statements share that prefix. `StructuralKey::complete` now says whether the whole -statement was read. It is false when the parser stops early, when the body -holds notation the scheme has no rule for (`!`, `?`, `@` and `\` binders, -Isabelle's `\<…>` escapes, Lean 3's `$`), when a header drop discarded -the statement's own tokens, or when a leading bracket group was misread as -a binder telescope. It changes no key. The scan treats an +statement was read. It is false when the parser stops early or the input +ends inside an open bracket (ACL2s goals truncated mid-expression), when +the body holds notation the scheme has no rule for (`!`, `?`, `@` and `\` +binders, `~`, `==>`, Isabelle's `\<…>` escapes, Lean 3's `$`), when a +header drop discarded the statement's own tokens, or when a leading +bracket group was misread as a binder telescope. It changes no key. The +scan treats an incomplete key as no identity: such pairs are `unparsed`, and such statements take no part in shape joins. @@ -346,19 +348,19 @@ Share of each corpus read completely (`dk-shape-v1`, 2026-10-27): [cols="2,2,2,2,2",options="header"] |=== | Corpus | Distinct rows | Read completely | Keys shared by distinct statements | Homonymous names -| acl2 | 135963 | 25.6 % | 2063 | 7.9 % -| acl2s | 112677 | 88.1 % | 3576 | 4.7 % -| afp | 102683 | 10.8 % | 530 | 2.0 % -| agda | 46028 | 41.4 % | 585 | 8.6 % -| dafny | 10487 | 58.4 % | 202 | 12.1 % -| dedukti | 1453 | 77.4 % | 57 | 20.6 % -| hol4 | 95738 | 10.0 % | 130 | 4.1 % -| hol_light | 43937 | 2.5 % | 24 | 2.8 % -| isabelle_zf | 3577 | 0.3 % | 0 | 0.3 % -| lambda_prolog | 24897 | 94.0 % | 133 | 49.9 % -| lean3 | 92680 | 27.3 % | 2901 | 19.1 % -| mizar | 76522 | 20.5 % | 512 | 1.8 % -| why3 | 25180 | 30.5 % | 396 | 21.8 % +| acl2 | 135963 | 16.6 % | 822 | 8.0 % +| acl2s | 112677 | 5.4 % | 361 | 4.8 % +| afp | 102683 | 10.8 % | 525 | 2.1 % +| agda | 46028 | 41.3 % | 584 | 8.6 % +| dafny | 10487 | 58.2 % | 201 | 12.2 % +| dedukti | 1453 | 76.7 % | 56 | 20.6 % +| hol4 | 95738 | 9.0 % | 109 | 4.2 % +| hol_light | 43937 | 2.0 % | 19 | 2.9 % +| isabelle_zf | 3577 | 0.4 % | 0 | 0.3 % +| lambda_prolog | 24897 | 94.0 % | 130 | 50.0 % +| lean3 | 92680 | 27.1 % | 2875 | 19.2 % +| mizar | 76522 | 20.3 % | 498 | 1.8 % +| why3 | 25180 | 29.8 % | 390 | 21.9 % |=== "Keys shared by distinct statements" counts complete keys only. Most are @@ -392,7 +394,8 @@ than changed under `dk-shape-v1`: in positive positions; the probes found no pair merged by that alone. `complete` now flags the header drop, the keyword drop, unread notation, -∃ (the parser stops) and the telescope misread. It does not flag the +∃ (the parser stops), truncation inside a group and the telescope +misread. It does not flag the short-name rule or the hypothesis-as-sort rule, which produce well-formed but wrong shapes; the scan's `informative` filter catches the short-name rule's commonest form (a variable in function position). The corpus @@ -401,15 +404,15 @@ identity keys (E6 `cross_prover_identity_key`) inherit all four causes. === What the measurement found in the corpora Over all 33 pairs: 203,860 same-name statement pairs, of which 1,070 are -exact cognates, 3,619 shape cognates, 76 skeleton (specialisation) -candidates, 36,470 differ, and 162,625 (80 %) are `unparsed`. Synonym -candidates under different names: 269 by identical text, 848 by shape, -882 by skeleton. Debug build: 171 s for all thirteen corpora, almost all +exact cognates, 2,771 shape cognates, 71 skeleton (specialisation) +candidates, 8,414 differ, and 191,534 (94 %) are `unparsed`. Synonym +candidates under different names: 269 by identical text, 495 by shape, +871 by skeleton. Debug build: 182 s for all thirteen corpora, almost all of it loading and canonicalising; one pair scans in about a second. * *HOL4 ↔ HOL Light* (pilot pair): 1,033 exact cognates and 144 text - synonyms (`FACT_0` / `pth_0`), but 5,550 same-name pairs `unparsed`: - `dk-shape-v1` reads 2.5 % of HOL Light. The pilot pair needs HOL + synonyms (`FACT_0` / `pth_0`), but 5,554 same-name pairs `unparsed`: + `dk-shape-v1` reads 2 % of HOL Light. The pilot pair needs HOL notation in the canonicaliser before shape evidence means anything. * *Lean 3 ↔ AFP, AFP ↔ Mizar, Lean 3 ↔ Mizar*: the synonym joins find real cross-family correspondences: `sqrt_zero ~ lemSqrt0`, @@ -425,7 +428,7 @@ of it loading and canonicalising; one pair scans in about a second. short-name rule above), fewer than three constants, or a bare type signature (λProlog's `int -> int -> int` against Dedukti's `Int -> Int -> Int`) say nothing about which statement it is. Joins - between different names skip them (3,749 groups, counted). + between different names skip them (3,415 groups, counted). === Equivalence by invariant and by witness diff --git a/src/rust/corpus/canonical.rs b/src/rust/corpus/canonical.rs index 0f8e8ba8..38e2d3ca 100644 --- a/src/rust/corpus/canonical.rs +++ b/src/rust/corpus/canonical.rs @@ -130,7 +130,8 @@ pub struct StructuralKey { pub tier: KeyTier, /// Whether the shape accounts for the whole statement. False when the /// parser stopped early (anything but a trailing `.`/`,`/`;` or an - /// unmatched closing bracket left over), when the body holds notation + /// unmatched closing bracket left over), when the input ended inside an + /// open bracket (a statement truncated mid-group), when the body holds notation /// this scheme has no rule for ([`is_unread_notation`]), when the header /// drop discarded tokens that were not a declared head, or when a leading /// bracket group was misread as a binder telescope. In each case the @@ -869,11 +870,20 @@ struct Parser { toks: Vec, i: usize, varmap: std::collections::HashMap, + /// Opening brackets the input ended before closing: a statement + /// truncated inside a group (`(x = y`) parses to the end and would + /// otherwise look complete. + unclosed: usize, } impl Parser { fn new(toks: Vec, varmap: std::collections::HashMap) -> Self { - Parser { toks, i: 0, varmap } + Parser { + toks, + i: 0, + varmap, + unclosed: 0, + } } fn peek(&self) -> Option<&Tk> { @@ -908,6 +918,8 @@ impl Parser { let inner = self.expr(0); if matches!(self.peek(), Some(Tk::Close(_))) { self.i += 1; + } else if self.peek().is_none() { + self.unclosed += 1; } Some(inner) }, @@ -1142,13 +1154,25 @@ fn number_variables(body: &[Tk], bound: &Binders) -> std::collections::HashMap` symbol escapes (which lex as -/// `\`, `<`, name, `>`), and Lean 3's `$` application. The parser reads them -/// as plain names and consumes them, so a shape can look complete and still -/// be wrong; their presence marks the key incomplete. Over-cautious by -/// design: Lean's `s \ t` set difference is flagged too. +/// `?`, `@` and `\` binders and `~` negation, Isabelle's `\<…>` symbol +/// escapes (which lex as `\`, `<`, name, `>`), and Lean 3's `$` application. +/// The parser reads them as plain names and consumes them, so a shape can +/// look complete and still be wrong; their presence marks the key +/// incomplete. Over-cautious by design: Lean's `s \ t` set difference is +/// flagged too. fn is_unread_notation(t: &Tk) -> bool { - matches!(t, Tk::Sym(s) if matches!(s.as_str(), "\\" | "!" | "?" | "@" | "$")) + matches!(t, Tk::Sym(s) if matches!(s.as_str(), "\\" | "!" | "?" | "@" | "$" | "~")) +} + +/// Whether the body holds unread notation: a token [`is_unread_notation`] +/// names, or HOL's `==>` implication, which the lexer splits into `==` and +/// `>` (the shape it then renders is an equality applied to a comparison). +/// The lexer is left alone so that no key changes; only the flag sees it. +fn has_unread_notation(body: &[Tk]) -> bool { + body.iter().any(is_unread_notation) + || body + .windows(2) + .any(|w| matches!((&w[0], &w[1]), (Tk::Sym(a), Tk::Sym(b)) if a == "==" && b == ">")) } /// Both canonical forms from one pass, and whether the shape accounts for @@ -1161,10 +1185,14 @@ fn normalise(statement: &str) -> (String, String, bool) { let toks = drop_ascriptions(&toks); let (body, bound) = extract_binders(&toks); let varmap = number_variables(&body, &bound); - let unread = body.iter().any(is_unread_notation); + let unread = has_unread_notation(&body); let mut parser = Parser::new(body, varmap); let ast = parser.expr(0); - let complete = parser.rest_is_ignorable() && !unread && !dropped_body && !bound.misread; + let complete = parser.rest_is_ignorable() + && parser.unclosed == 0 + && !unread + && !dropped_body + && !bound.misread; let core = render(&ast, false); let skel = render(&ast, true); @@ -1406,10 +1434,16 @@ mod tests { #[test] fn unread_notation_and_early_stops_are_incomplete() { for s in [ - // HOL binders + // HOL binders, negation and implication (`==>` lexes as `==` `>`) "!m n. m + n = n + m", "?x. x = 0", "(\\x. x) = I", + "~F", + "F ==> T", + // truncated inside a group: the parser reaches the end with the + // group still open + "(x = y", + "(implies (and (bvp m) (< (len m) (expt 2 64))", // Isabelle ASCII symbol escapes "x \\ y \\ f x = f y", // Lean 3 `$` diff --git a/src/rust/lexicon/scan.rs b/src/rust/lexicon/scan.rs index 241fde99..5c53a870 100644 --- a/src/rust/lexicon/scan.rs +++ b/src/rust/lexicon/scan.rs @@ -149,6 +149,10 @@ pub fn validate_corpus_key(key: &str) -> Result<()> { { bail!("corpus key `{key}` must be non-empty [a-z0-9_]"); } + // `pairs/__.jsonl` is unambiguous only if no key contains `__`. + if key.contains("__") { + bail!("corpus key `{key}` must not contain `__`"); + } Ok(()) } @@ -1076,6 +1080,17 @@ pub fn run(opts: &RunOptions) -> Result { fs::create_dir_all(&pairs_dir).with_context(|| format!("create {}", pairs_dir.display()))?; fs::create_dir_all(&collisions_dir) .with_context(|| format!("create {}", collisions_dir.display()))?; + // A re-run over a different pair set must not leave the previous run's + // files beside this run's summary. Only the scan's own `.jsonl` files + // are removed; anything else in the directory is left alone. + for dir in [&pairs_dir, &collisions_dir] { + for entry in fs::read_dir(dir).with_context(|| format!("read {}", dir.display()))? { + let path = entry?.path(); + if path.extension().and_then(|e| e.to_str()) == Some("jsonl") { + fs::remove_file(&path).with_context(|| format!("remove {}", path.display()))?; + } + } + } let coverage: Vec = corpora.values().map(Corpus::coverage).collect(); write_lines(&opts.out.join("coverage.jsonl"), &coverage)?; @@ -1164,6 +1179,8 @@ mod tests { assert!(parse_pair("hol4").is_err()); assert!(parse_pair("hol4:hol4").is_err()); assert!(parse_pair("../etc:hol4").is_err()); + // `a__b:c` and `a:b__c` would both write pairs/a__b__c.jsonl + assert!(parse_pair("a__b:c").is_err()); } #[test] diff --git a/src/rust/main.rs b/src/rust/main.rs index 73c3857a..197e1bca 100644 --- a/src/rust/main.rs +++ b/src/rust/main.rs @@ -1400,7 +1400,12 @@ fn lexicon_command(op: LexiconOp) -> Result<()> { } for p in &pairs { let pair = scan::parse_pair(p)?; - if !all_pairs.contains(&pair) { + // A pair is the same pair in either direction; the first spelling + // requested is the one scanned. + let seen = all_pairs + .iter() + .any(|(a, b)| (a, b) == (&pair.0, &pair.1) || (a, b) == (&pair.1, &pair.0)); + if !seen { all_pairs.push(pair); } } diff --git a/tests/lexicon_scan_test.rs b/tests/lexicon_scan_test.rs index 5acc03b5..4b3033e0 100644 --- a/tests/lexicon_scan_test.rs +++ b/tests/lexicon_scan_test.rs @@ -199,3 +199,37 @@ fn unknown_corpus_keys_fail_loudly() { assert!(Corpus::load(&fixtures(), "no_such_corpus").is_err()); assert!(Corpus::load(&fixtures(), "../etc").is_err()); } + +#[test] +fn a_rerun_with_fewer_pairs_leaves_no_stale_pair_files() { + let out = std::env::temp_dir().join(format!("echidna-lexicon-rerun-{}", std::process::id())); + let run_with = |pairs: Vec<(String, String)>| { + scan::run(&RunOptions { + training_dir: fixtures(), + pairs, + out: out.clone(), + scan: ScanOptions::default(), + collision_samples: 10, + }) + .expect("run") + }; + run_with(vec![ + ("lean_mini".into(), "isabelle_mini".into()), + ("hol4_mini".into(), "hol_light_mini".into()), + ]); + run_with(vec![("lean_mini".into(), "isabelle_mini".into())]); + let listed = |dir: &str| { + let mut names: Vec = std::fs::read_dir(out.join(dir)) + .unwrap() + .map(|e| e.unwrap().file_name().to_string_lossy().into_owned()) + .collect(); + names.sort(); + names + }; + assert_eq!(listed("pairs"), vec!["lean_mini__isabelle_mini.jsonl"]); + assert_eq!( + listed("collisions"), + vec!["isabelle_mini.jsonl", "lean_mini.jsonl"] + ); + let _ = std::fs::remove_dir_all(&out); +} From 157cda2f60cb53d2a68d54eabc78a125cbf9a6da Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 27 Oct 2026 04:56:20 +0000 Subject: [PATCH 06/16] fix(corpus): bound parser nesting; corpus identity skips incomplete keys Addresses the CodeRabbit review of #453. - The canonicaliser's parser recurses once per bracket level and runs on the caller's stack from `corpus ingest` and octad export, so a statement nested deeply enough overflowed it (50,000 levels aborts the test thread on the previous code). Nesting is now cut off at 256 levels: the group becomes a hole and the key is marked incomplete. The shipped corpora reach a depth in the fifties, so no key changes. - `corpus identity` groups only complete keys, as docs/CORPUS.adoc says it should, and reports how many matching declarations it skipped. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_01WS4mfQeC3N1DWjcCQJaQqw --- CHANGELOG.adoc | 5 ++++- docs/CORPUS.adoc | 3 ++- src/rust/corpus/canonical.rs | 38 ++++++++++++++++++++++++++++++++++++ src/rust/main.rs | 13 ++++++++++++ 4 files changed, 57 insertions(+), 2 deletions(-) diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index 79e78c71..a2c48ba8 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -31,7 +31,10 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning]. parser stops early or the input ends inside an open bracket, meets notation `+dk-shape-v1+` has no rule for (HOL binders, `+~+`, `+==>+`, Isabelle `+\<…>+` escapes), drops a statement's own leading tokens as a - "header", or misreads a leading group as a telescope. No key changes. + "header", misreads a leading group as a telescope, or cuts off nesting + deeper than 256 levels (the parser is now bounded, so a deeply nested + statement cannot overflow a caller's stack). `+corpus identity+` skips + incomplete declarations and says how many. No key changes. Measured on `+training_data/+`, 0.4 %–94 % of a corpus is read completely; the rule-level causes are recorded for a `+dk-shape-v2+` decision in `+docs/decisions/2026-10-19-lexicon-v2-and-identity-arbitration.adoc+`. diff --git a/docs/CORPUS.adoc b/docs/CORPUS.adoc index 52b25b40..b54c5d01 100644 --- a/docs/CORPUS.adoc +++ b/docs/CORPUS.adoc @@ -248,7 +248,8 @@ says whether the canonicaliser read the *whole* statement; when it did not and `+?+` binders, Isabelle's `+\<…>+` escapes — or a header drop discarded the statement's own leading tokens), the key is still reported at the structural tier but is a *prefix* that other statements share. Treat an -incomplete key as no identity at all. Measured on `+training_data/+`, the +incomplete key as no identity at all: `+corpus identity+` skips such +declarations and reports how many it skipped. Measured on `+training_data/+`, the share of statements read completely ranges from under 1% (Isabelle/ZF) to over 90% (λProlog); see `+docs/decisions/2026-10-19-lexicon-v2-and-identity-arbitration.adoc+` diff --git a/src/rust/corpus/canonical.rs b/src/rust/corpus/canonical.rs index 38e2d3ca..25c0d95d 100644 --- a/src/rust/corpus/canonical.rs +++ b/src/rust/corpus/canonical.rs @@ -874,8 +874,19 @@ struct Parser { /// truncated inside a group (`(x = y`) parses to the end and would /// otherwise look complete. unclosed: usize, + /// Current bracket nesting, bounded by [`MAX_NESTING`]. + depth: usize, + /// A group deeper than [`MAX_NESTING`] was skipped as a hole. + too_deep: bool, } +/// Deepest bracket nesting the parser descends into. Each level costs three +/// stack frames (`expr` → `app` → `atom`), and `structural_key` runs on the +/// caller's stack (`corpus ingest`, octad export), so a statement nested +/// deeper than this is cut off rather than allowed to overflow it. The +/// shipped corpora reach a depth in the fifties. +const MAX_NESTING: usize = 256; + impl Parser { fn new(toks: Vec, varmap: std::collections::HashMap) -> Self { Parser { @@ -883,6 +894,8 @@ impl Parser { i: 0, varmap, unclosed: 0, + depth: 0, + too_deep: false, } } @@ -914,8 +927,16 @@ impl Parser { let t = self.peek()?.clone(); match t { Tk::Open(_) => { + if self.depth >= MAX_NESTING { + // Skip the whole group; the key is marked incomplete. + self.too_deep = true; + self.i = matching(&self.toks, self.i) + 1; + return Some(Node::Hole); + } + self.depth += 1; self.i += 1; let inner = self.expr(0); + self.depth -= 1; if matches!(self.peek(), Some(Tk::Close(_))) { self.i += 1; } else if self.peek().is_none() { @@ -1190,6 +1211,7 @@ fn normalise(statement: &str) -> (String, String, bool) { let ast = parser.expr(0); let complete = parser.rest_is_ignorable() && parser.unclosed == 0 + && !parser.too_deep && !unread && !dropped_body && !bound.misread; @@ -1503,6 +1525,22 @@ mod tests { assert!(structural_key("(x y : nat) : x + y = y + x").complete); } + /// Nesting past `MAX_NESTING` is cut off and marked incomplete instead + /// of recursing once per level. Fifty thousand levels would overflow a + /// test thread's stack without the bound; within the bound keys are as + /// before. + #[test] + fn nesting_is_bounded() { + let deep = format!("{}x{}", "(".repeat(50_000), ")".repeat(50_000)); + let k = structural_key(&deep); + assert!(!k.complete); + assert_eq!(k.key.len(), 64); + let shallow = format!("{}x = y{}", "(".repeat(60), ")".repeat(60)); + let s = structural_key(&shallow); + assert!(s.complete, "{}", s.shape); + assert_eq!(s.key, structural_key("x = y").key); + } + /// The guard is a no-op on balanced input: keys stay as they were. #[test] fn balanced_input_keys_are_unchanged_by_the_bracket_guard() { diff --git a/src/rust/main.rs b/src/rust/main.rs index 197e1bca..68a033d6 100644 --- a/src/rust/main.rs +++ b/src/rust/main.rs @@ -1812,6 +1812,9 @@ fn corpus_command(op: CorpusOp, formatter: &OutputFormatter) -> Result<()> { Vec<(String, String)>, ), > = std::collections::BTreeMap::new(); + // A key the canonicaliser did not derive from the whole statement + // is a shared prefix, not an identity (docs/CORPUS.adoc). + let mut skipped_incomplete = 0usize; for entry in &corpus.entries { let matches = everything || entry.qualified.to_lowercase().contains(&needle) @@ -1820,6 +1823,10 @@ fn corpus_command(op: CorpusOp, formatter: &OutputFormatter) -> Result<()> { continue; } let key = echidna::corpus::canonical::structural_key(&entry.statement); + if !key.complete { + skipped_incomplete += 1; + continue; + } let slot = groups .entry(key.key.clone()) .or_insert_with(|| (key, Vec::new())); @@ -1827,6 +1834,12 @@ fn corpus_command(op: CorpusOp, formatter: &OutputFormatter) -> Result<()> { .push((corpus.adapter.clone(), entry.qualified.clone())); } + if skipped_incomplete > 0 { + formatter.info(&format!( + "{skipped_incomplete} matching declaration(s) skipped: the canonicaliser \ + did not read their statement completely, so they carry no identity" + ))?; + } if groups.is_empty() { formatter.info(&format!("no declarations matching '{}'", pattern))?; return Ok(()); From 58c5ad8575ca82b1d57bf720c58592f77bcbc3fe Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 27 Oct 2026 04:57:37 +0000 Subject: [PATCH 07/16] perf(corpus): drop_ascriptions no longer scans to the close of every group An ascription group is exactly `( x :: sort )`, so a group whose second token is not `::` cannot be one; it is now passed through without the `matching` scan that made the pass quadratic on deeply nested input (the 50,000-level nesting test took 96 s). Same output on every input, so no key changes. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_01WS4mfQeC3N1DWjcCQJaQqw --- src/rust/corpus/canonical.rs | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/rust/corpus/canonical.rs b/src/rust/corpus/canonical.rs index 25c0d95d..16873432 100644 --- a/src/rust/corpus/canonical.rs +++ b/src/rust/corpus/canonical.rs @@ -823,6 +823,15 @@ fn drop_ascriptions(toks: &[Tk]) -> Vec { let mut i = 0usize; while i < toks.len() { if is_open(&toks[i]) { + // Only `( x :: sort )` qualifies, so a group without `::` in second + // place is left alone without scanning for its close (that scan + // made this quadratic on deeply nested input). + let could_ascribe = matches!(toks.get(i + 2), Some(Tk::Sym(s)) if s == "::"); + if !could_ascribe { + out.push(toks[i].clone()); + i += 1; + continue; + } let j = matching(toks, i); let inner: Vec = between(toks, i, j).to_vec(); let ids: Vec<&String> = inner From 4ff212a92ef08c9f926d410ca108cdf6ebbda9d9 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 27 Oct 2026 05:04:12 +0000 Subject: [PATCH 08/16] docs(lexicon): record D8, the bridge/octad identity-key ruling Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_01WS4mfQeC3N1DWjcCQJaQqw --- .../2026-10-19-lexicon-v2-and-identity-arbitration.adoc | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/docs/decisions/2026-10-19-lexicon-v2-and-identity-arbitration.adoc b/docs/decisions/2026-10-19-lexicon-v2-and-identity-arbitration.adoc index 73b4d5e3..ab377809 100644 --- a/docs/decisions/2026-10-19-lexicon-v2-and-identity-arbitration.adoc +++ b/docs/decisions/2026-10-19-lexicon-v2-and-identity-arbitration.adoc @@ -2,7 +2,7 @@ // SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) = ADR: lexicon v2 (false friends, phrases, equivalences) and hub-and-probe identity arbitration (stage 6c) :revdate: 2026-10-19 -:status: accepted in part — D1, D2 and D4 ruled 2026-10-19 (§7); D3, D5, D6 and D7 open +:status: accepted in part — D1, D2 and D4 ruled 2026-10-19, D8 ruled 2026-10-27 (§7); D3, D5, D6 and D7 open == Context (measured on `main` at `ed6ef60`, 2026-10-19) @@ -487,7 +487,7 @@ and ABI changes, kernel translation) wait for the stronger model. Ruled PR 6 (superseded in practice by #449's canonicaliser, see PR 3 results), the scan covers one corpus per family plus one in-family pair each, its records carry UUIDv8 ids, the invariant/witness reading goes in this ADR, -and phrase detection follows PR 3. D6 and D7 opened 2026-10-27. +and phrase detection follows PR 3. D6 and D7 opened, and D8 ruled, 2026-10-27. [cols="1,5,3,3",options="header"] |=== @@ -499,6 +499,7 @@ and phrase detection follows PR 3. D6 and D7 opened 2026-10-27. | D5 | Open the verisimdb consonance-subject issue (option E) now? | Yes | open | D6 | Fix `dk-shape-v1`'s four rule-level false-identity causes (header drop, keyword drop, short names as variables, unread notation and binders) as `dk-shape-v2`, bumping `SCHEME` and so every corpus identity key? | Yes, as its own PR, starting with the header and keyword drops (smallest, largest effect), with the scan as the before/after measure | open | D7 | Fix the `training_data/` extractors for ACL2 (hints, escape codes) and ACL2s (truncation, comment lines), and strip proof bodies from Lean 3 goals? | Yes, at the extractors, then re-scan | open +| D8 | The VeriSim bridge and the octad export write `cross_prover_identity_key` for every declaration, incomplete keys included, and consumers join on equality (CodeRabbit on #453; predates this stack, from #449). Make the keys `Option`, or add a flag? | Additive `identity_complete: bool` on `DeclGraph` and `GraphPayload`, own PR | As recommended, 2026-10-27: additive flag, serde default and an added capnp field, key fields unchanged, consumers filter on it; own PR after #453, ER schema doc updated. The `Option` shape waits for D6. |=== == Non-claims From d66827abbdeb9b3d01a47a736f24c1cf7fc2b6d6 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 27 Oct 2026 05:13:28 +0000 Subject: [PATCH 09/16] fix(corpus): complete catches invented operands, unclosed wrappers and notation in binder sorts; text join counts lexical tokens MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - A key whose AST contains a hole (a missing operand) is incomplete. - An unbalanced `(assert …` wrapper marks the key incomplete. - Unread notation is detected before binder extraction, so notation inside a binder sort is no longer hidden. - The text synonym join counts lexical tokens rather than words. - ADR coverage table and totals refreshed from a full rescan. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01WS4mfQeC3N1DWjcCQJaQqw --- ...9-lexicon-v2-and-identity-arbitration.adoc | 53 ++++++------- src/rust/corpus/canonical.rs | 76 +++++++++++++++++-- src/rust/lexicon/scan.rs | 10 ++- 3 files changed, 104 insertions(+), 35 deletions(-) diff --git a/docs/decisions/2026-10-19-lexicon-v2-and-identity-arbitration.adoc b/docs/decisions/2026-10-19-lexicon-v2-and-identity-arbitration.adoc index ab377809..a0a03c2b 100644 --- a/docs/decisions/2026-10-19-lexicon-v2-and-identity-arbitration.adoc +++ b/docs/decisions/2026-10-19-lexicon-v2-and-identity-arbitration.adoc @@ -333,13 +333,14 @@ The second finding is larger. When the canonicaliser cannot read a statement it rarely falls back to its text tier; it returns a *structural-tier* key for the prefix it did read, and different statements share that prefix. `StructuralKey::complete` now says whether the whole -statement was read. It is false when the parser stops early or the input -ends inside an open bracket (ACL2s goals truncated mid-expression), when -the body holds notation the scheme has no rule for (`!`, `?`, `@` and `\` -binders, `~`, `==>`, Isabelle's `\<…>` escapes, Lean 3's `$`), when a -header drop discarded the statement's own tokens, or when a leading -bracket group was misread as a binder telescope. It changes no key. The -scan treats an +statement was read. It is false when the parser stops early, invents a +missing operand (`x + 1 =`) or reaches the end inside an open bracket or +an unclosed `(assert …` wrapper (ACL2s goals truncated mid-expression), +when the statement holds notation the scheme has no rule for (`!`, `?`, +`@` and `\` binders, `~`, `==>`, Isabelle's `\<…>` escapes, Lean 3's `$`; +checked before binders and ascriptions are removed), when a header drop +discarded the statement's own tokens, or when a leading bracket group was +misread as a binder telescope. It changes no key. The scan treats an incomplete key as no identity: such pairs are `unparsed`, and such statements take no part in shape joins. @@ -348,19 +349,19 @@ Share of each corpus read completely (`dk-shape-v1`, 2026-10-27): [cols="2,2,2,2,2",options="header"] |=== | Corpus | Distinct rows | Read completely | Keys shared by distinct statements | Homonymous names -| acl2 | 135963 | 16.6 % | 822 | 8.0 % -| acl2s | 112677 | 5.4 % | 361 | 4.8 % -| afp | 102683 | 10.8 % | 525 | 2.1 % -| agda | 46028 | 41.3 % | 584 | 8.6 % -| dafny | 10487 | 58.2 % | 201 | 12.2 % -| dedukti | 1453 | 76.7 % | 56 | 20.6 % -| hol4 | 95738 | 9.0 % | 109 | 4.2 % -| hol_light | 43937 | 2.0 % | 19 | 2.9 % +| acl2 | 135963 | 16.1 % | 798 | 8.0 % +| acl2s | 112677 | 5.3 % | 352 | 4.8 % +| afp | 102683 | 10.7 % | 522 | 2.1 % +| agda | 46028 | 41.0 % | 578 | 8.6 % +| dafny | 10487 | 53.8 % | 154 | 12.2 % +| dedukti | 1453 | 76.0 % | 54 | 20.6 % +| hol4 | 95738 | 8.7 % | 107 | 4.2 % +| hol_light | 43937 | 1.9 % | 15 | 2.9 % | isabelle_zf | 3577 | 0.4 % | 0 | 0.3 % -| lambda_prolog | 24897 | 94.0 % | 130 | 50.0 % -| lean3 | 92680 | 27.1 % | 2875 | 19.2 % -| mizar | 76522 | 20.3 % | 498 | 1.8 % -| why3 | 25180 | 29.8 % | 390 | 21.9 % +| lambda_prolog | 24897 | 93.6 % | 122 | 50.0 % +| lean3 | 92680 | 26.5 % | 2777 | 19.2 % +| mizar | 76522 | 20.0 % | 477 | 1.8 % +| why3 | 25180 | 28.5 % | 378 | 21.9 % |=== "Keys shared by distinct statements" counts complete keys only. Most are @@ -404,15 +405,15 @@ identity keys (E6 `cross_prover_identity_key`) inherit all four causes. === What the measurement found in the corpora Over all 33 pairs: 203,860 same-name statement pairs, of which 1,070 are -exact cognates, 2,771 shape cognates, 71 skeleton (specialisation) -candidates, 8,414 differ, and 191,534 (94 %) are `unparsed`. Synonym -candidates under different names: 269 by identical text, 495 by shape, -871 by skeleton. Debug build: 182 s for all thirteen corpora, almost all +exact cognates, 2,708 shape cognates, 71 skeleton (specialisation) +candidates, 7,854 differ, and 192,157 (94 %) are `unparsed`. Synonym +candidates under different names: 315 by identical text, 491 by shape, +865 by skeleton. Debug build: 179 s for all thirteen corpora, almost all of it loading and canonicalising; one pair scans in about a second. * *HOL4 ↔ HOL Light* (pilot pair): 1,033 exact cognates and 144 text - synonyms (`FACT_0` / `pth_0`), but 5,554 same-name pairs `unparsed`: - `dk-shape-v1` reads 2 % of HOL Light. The pilot pair needs HOL + synonyms (`FACT_0` / `pth_0`), but 5,555 same-name pairs `unparsed`: + `dk-shape-v1` reads 1.9 % of HOL Light. The pilot pair needs HOL notation in the canonicaliser before shape evidence means anything. * *Lean 3 ↔ AFP, AFP ↔ Mizar, Lean 3 ↔ Mizar*: the synonym joins find real cross-family correspondences: `sqrt_zero ~ lemSqrt0`, @@ -428,7 +429,7 @@ of it loading and canonicalising; one pair scans in about a second. short-name rule above), fewer than three constants, or a bare type signature (λProlog's `int -> int -> int` against Dedukti's `Int -> Int -> Int`) say nothing about which statement it is. Joins - between different names skip them (3,415 groups, counted). + between different names skip them (3,335 groups, counted). === Equivalence by invariant and by witness diff --git a/src/rust/corpus/canonical.rs b/src/rust/corpus/canonical.rs index 16873432..441efe3e 100644 --- a/src/rust/corpus/canonical.rs +++ b/src/rust/corpus/canonical.rs @@ -528,15 +528,22 @@ fn drop_declared_head(toks: Vec) -> (Vec, bool) { } /// `(assert (forall …))` → `(forall …)`. -fn unwrap_assert(toks: Vec) -> Vec { +/// +/// The second value reports a wrapper that was unwrapped although its +/// closing bracket is missing (`(assert x y`): [`matching`]'s fallback +/// index is the last token, which also passes the "closes at the end" +/// test, so the wrapper is unwrapped as before (no key changes) and the +/// key is reported incomplete through [`StructuralKey::complete`]. +fn unwrap_assert(toks: Vec) -> (Vec, bool) { let mut cur = toks; + let mut unbalanced = false; loop { if !cur.first().map(is_open).unwrap_or(false) { - return cur; + return (cur, unbalanced); } let j = matching(&cur, 0); if j + 1 != cur.len() { - return cur; + return (cur, unbalanced); } let inner = between(&cur, 0, j).to_vec(); let head_is_assert = match inner.first() { @@ -547,12 +554,33 @@ fn unwrap_assert(toks: Vec) -> Vec { _ => false, }; if !head_is_assert { - return cur; + return (cur, unbalanced); + } + if matching_exact(&cur, 0).is_none() { + unbalanced = true; } cur = inner[1..].to_vec(); } } +/// Index of the bracket matching `toks[at]`, or `None` when the group is +/// never closed. [`matching`] returns the last index in that case, which +/// callers that need to tell the two apart cannot use. +fn matching_exact(toks: &[Tk], at: usize) -> Option { + let mut depth = 0usize; + for (j, t) in toks.iter().enumerate().skip(at) { + if is_open(t) { + depth += 1; + } else if is_close(t) { + depth = depth.saturating_sub(1); + if depth == 0 { + return Some(j); + } + } + } + None +} + /// The statement body with any declaration header and proof body removed, and /// whether the header drop discarded tokens that were not a declared head: /// a bracket drop (see [`drop_declared_head`]), or a declaration keyword @@ -560,7 +588,7 @@ fn unwrap_assert(toks: Vec) -> Vec { /// statement that merely *starts* with one (HOL4's `FACT 1 = 1`, keyed as /// `1 = 1`) loses it; without a following colon nothing was declared. fn strip_header(toks: &[Tk]) -> (Vec, bool) { - let mut cur = unwrap_assert(glue_agda_operators(toks)); + let (mut cur, unbalanced_wrapper) = unwrap_assert(glue_agda_operators(toks)); // declaration keyword + declared name let mut dropped_kw = false; loop { @@ -596,7 +624,10 @@ fn strip_header(toks: &[Tk]) -> (Vec, bool) { }; let keyword_unexplained = dropped_kw && !colon_at_top(&cur); let (body, head_unexplained) = drop_declared_head(cur); - (body, head_unexplained || keyword_unexplained) + ( + body, + head_unexplained || keyword_unexplained || unbalanced_wrapper, + ) } /// `x y : Nat` → (["x","y"], NAT); SMT-LIB `x Nat` likewise. @@ -1086,6 +1117,17 @@ impl Parser { } } +/// Whether the parser had to invent a node: a missing operand after a +/// trailing operator (`x + 1 =`), or a group it refused to descend into. +/// Either way the shape does not describe the statement. +fn has_hole(node: &Node) -> bool { + match node { + Node::Hole => true, + Node::Op(_, kids) | Node::App(kids) => kids.iter().any(has_hole), + _ => false, + } +} + fn render(node: &Node, skeleton: bool) -> String { match node { Node::Var(s) | Node::Name(s) | Node::Num(s) => s.clone(), @@ -1212,13 +1254,16 @@ fn has_unread_notation(body: &[Tk]) -> bool { /// consumed the body. fn normalise(statement: &str) -> (String, String, bool) { let (toks, dropped_body) = strip_header(&lex(statement)); + // Checked before ascriptions and binders are removed: a binder's sort + // can hold notation too (`(x : F $ A)`), and extraction would drop it. + let unread = has_unread_notation(&toks); let toks = drop_ascriptions(&toks); let (body, bound) = extract_binders(&toks); let varmap = number_variables(&body, &bound); - let unread = has_unread_notation(&body); let mut parser = Parser::new(body, varmap); let ast = parser.expr(0); - let complete = parser.rest_is_ignorable() + let complete = !has_hole(&ast) + && parser.rest_is_ignorable() && parser.unclosed == 0 && !parser.too_deep && !unread @@ -1286,6 +1331,12 @@ pub fn structural_key(statement: &str) -> StructuralKey { /// /// Falls back to the lower-cased source tokens when the statement does not /// parse, so every declaration contributes *something*. +/// Number of lexical tokens in `statement`, punctuation counted: `f(x)=g(x)` +/// is eight. For callers that need "how much is here" without a parse. +pub fn token_count(statement: &str) -> usize { + lex(statement).len() +} + pub fn canonical_tokens(statement: &str) -> Vec { let shape = canonical_shape(statement); let source = if shape.is_empty() { @@ -1475,6 +1526,15 @@ mod tests { // group still open "(x = y", "(implies (and (bvp m) (< (len m) (expt 2 64))", + // truncated after an operator: the parser invents the operand + "x + 1 =", + "forall x : nat, x = x /\\", + // a wrapper whose close is missing is still unwrapped (no key + // change) and reported + "(assert x y", + "(assert (forall ((x Nat)) (= x x", + // notation inside a binder's sort is dropped by extraction + "forall (x : F $ A), x + 0 = x", // Isabelle ASCII symbol escapes "x \\ y \\ f x = f y", // Lean 3 `$` diff --git a/src/rust/lexicon/scan.rs b/src/rust/lexicon/scan.rs index 5c53a870..cfbc0a31 100644 --- a/src/rust/lexicon/scan.rs +++ b/src/rust/lexicon/scan.rs @@ -927,7 +927,7 @@ pub fn scan_pair( summary.text_groups_capped += 1; continue; } - if text.split_whitespace().count() < 3 { + if canonical::token_count(text) < 3 { summary.text_groups_uninformative += 1; continue; } @@ -1218,6 +1218,14 @@ mod tests { assert!(informative("(ARROW (LE v0 v1) (LE (ADD v0 1) (ADD v1 1)))")); } + #[test] + fn text_join_counts_lexical_tokens_not_words() { + // one whitespace field, eight tokens: enough to join two names on + assert!(canonical::token_count("f(x)=g(x)") >= 3); + assert!(canonical::token_count("T") < 3); + assert!(canonical::token_count("x = y") >= 3); + } + #[test] fn pair_ids_ignore_side_order() { let x = ("hol4", "ADD_COMM", "!m n. m + n = n + m"); From fa740866f869606d7f4db75d3452a88e69170f09 Mon Sep 17 00:00:00 2001 From: "coderabbitai[bot]" <136622811+coderabbitai[bot]@users.noreply.github.com> Date: Tue, 27 Oct 2026 05:21:21 +0000 Subject: [PATCH 10/16] docs(lexicon): clarify scan contracts, canonical parsing limits, and CLI errors --- src/rust/corpus/canonical.rs | 20 +++++-- src/rust/lexicon/scan.rs | 113 +++++++++++++++++++++++++++++------ src/rust/main.rs | 8 ++- 3 files changed, 117 insertions(+), 24 deletions(-) diff --git a/src/rust/corpus/canonical.rs b/src/rust/corpus/canonical.rs index 16873432..454227d5 100644 --- a/src/rust/corpus/canonical.rs +++ b/src/rust/corpus/canonical.rs @@ -476,7 +476,7 @@ fn has_colon(toks: &[Tk]) -> bool { .any(|t| matches!(t, Tk::Sym(s) if s == ":" || s == "::")) } -/// Whether a top-level `:` occurs anywhere in `toks` (depth 0 relative to +/// Whether a top-level `:` or `::=` occurs in `toks` (depth 0 relative to /// the start of the slice). fn colon_at_top(toks: &[Tk]) -> bool { let mut depth = 0usize; @@ -556,9 +556,9 @@ fn unwrap_assert(toks: Vec) -> Vec { /// The statement body with any declaration header and proof body removed, and /// whether the header drop discarded tokens that were not a declared head: /// a bracket drop (see [`drop_declared_head`]), or a declaration keyword -/// with no top-level `:` after it. Keywords match case-insensitively, so a +/// with no top-level `:` or `::=` after it. Keywords match case-insensitively, so a /// statement that merely *starts* with one (HOL4's `FACT 1 = 1`, keyed as -/// `1 = 1`) loses it; without a following colon nothing was declared. +/// `1 = 1`) loses it; without either separator the drop is flagged. fn strip_header(toks: &[Tk]) -> (Vec, bool) { let mut cur = unwrap_assert(glue_agda_operators(toks)); // declaration keyword + declared name @@ -817,7 +817,8 @@ fn extract_binders(toks: &[Tk]) -> (Vec, Binders) { (out, bound) } -/// Isabelle's `(x :: nat)` is a term ascription, not a binder. +/// Unwrap Isabelle-style `(x :: nat)` ascriptions with recognised sorts, +/// retaining the term identifier. Other groups are preserved. fn drop_ascriptions(toks: &[Tk]) -> Vec { let mut out: Vec = Vec::new(); let mut i = 0usize; @@ -897,6 +898,7 @@ struct Parser { const MAX_NESTING: usize = 256; impl Parser { + /// Start at the first token, using `varmap` to map source names to canonical variables. fn new(toks: Vec, varmap: std::collections::HashMap) -> Self { Parser { toks, @@ -932,6 +934,10 @@ impl Parser { } } + /// Read an atom or bracketed expression, advancing the cursor. Return + /// `None` at end of input, before a closing bracket, or after consuming + /// `:`, `::`, `,` or `.`. Groups beyond the nesting limit become holes + /// and set `too_deep`; groups ending at EOF set `unclosed`. fn atom(&mut self) -> Option { let t = self.peek()?.clone(); match t { @@ -1209,7 +1215,8 @@ fn has_unread_notation(body: &[Tk]) -> bool { /// the whole statement: `(shape, skeleton, complete)`. Complete means the /// header drop discarded only a declared head, no leading group was misread /// as a telescope, the body holds no unread notation, and the parser -/// consumed the body. +/// left only ignorable terminators or closing brackets, with no group +/// left open at end of input or skipped beyond [`MAX_NESTING`]. fn normalise(statement: &str) -> (String, String, bool) { let (toks, dropped_body) = strip_header(&lex(statement)); let toks = drop_ascriptions(&toks); @@ -1259,6 +1266,9 @@ pub fn canonical_skeleton(statement: &str) -> String { /// The three tiers are tried in order: the shape as written; the shape with /// binders and sorts erased (covers provers that elide them); and finally /// whitespace-normalised text (covers statements that are not terms). +/// A partial parse can still yield a structural key; consult +/// [`StructuralKey::complete`] before treating it as the whole statement. +/// Text-tier keys always have `complete = false`. pub fn structural_key(statement: &str) -> StructuralKey { let (shape, skeleton, parsed_all) = normalise(statement); diff --git a/src/rust/lexicon/scan.rs b/src/rust/lexicon/scan.rs index 5c53a870..df4e068a 100644 --- a/src/rust/lexicon/scan.rs +++ b/src/rust/lexicon/scan.rs @@ -127,7 +127,12 @@ pub fn preset_pairs(preset: &str) -> Option> { } /// Parse a `A:B` pair argument. Both sides must be corpus keys as they -/// appear in `proof_states_.jsonl`. +/// appear in `proof_states_.jsonl`; their existence is not checked. +/// +/// # Errors +/// +/// The separator is missing, either key fails [`validate_corpus_key`], or +/// both keys are identical. Whitespace is not trimmed. pub fn parse_pair(arg: &str) -> Result<(String, String)> { let (a, b) = arg .split_once(':') @@ -140,7 +145,12 @@ pub fn parse_pair(arg: &str) -> Result<(String, String)> { Ok((a.to_string(), b.to_string())) } -/// Corpus keys become file names, so only `[a-z0-9_]` is accepted. +/// Validate a corpus key for use in scan file names. +/// +/// # Errors +/// +/// The key is empty, contains characters outside `[a-z0-9_]`, or contains +/// `__`, which is reserved as the separator in pair file names. pub fn validate_corpus_key(key: &str) -> Result<()> { if key.is_empty() || !key @@ -159,7 +169,8 @@ pub fn validate_corpus_key(key: &str) -> Result<()> { /// Fold a theorem name for cross-prover matching: keep the last component /// of a dotted or `::`-qualified name, lower-case it, read `-` as `_`, and /// trim surrounding underscores. `nat.add_comm`, `ADD_COMM` and `add-comm` -/// all fold to `add_comm`. +/// all fold to `add_comm`. A single `:` also separates components. If the +/// name ends in a separator, the whole name is used before folding. pub fn fold_name(name: &str) -> String { let tail = name.rsplit(['.', ':']).next().unwrap_or(name); let tail = if tail.is_empty() { name } else { tail }; @@ -244,6 +255,7 @@ pub struct Corpus { by_skeleton: BTreeMap>, } +/// Trim whitespace and replace each internal run with one space. fn collapse_whitespace(s: &str) -> String { s.split_whitespace().collect::>().join(" ") } @@ -251,7 +263,9 @@ fn collapse_whitespace(s: &str) -> String { impl Corpus { /// Build a corpus from `(name, statement)` rows. Names are trimmed, /// statement whitespace is collapsed, and rows with an empty side or a - /// duplicate of an earlier row are dropped. + /// duplicate of an earlier row are dropped. Entries are sorted by name + /// then statement; only complete keys enter the shape and skeleton + /// indices. The corpus key is stored without validation. pub fn from_rows(key: &str, rows: I) -> Self where I: IntoIterator, @@ -326,13 +340,15 @@ impl Corpus { } /// Load `training_dir/proof_states_.jsonl`, reading each line's - /// `theorem` and `goal` strings. + /// `theorem` and `goal` strings. Blank lines are ignored. Malformed JSON + /// increments `lines_malformed`; valid JSON without non-empty string + /// fields increments `lines_without_statement`. /// /// # Errors /// - /// The key is not `[a-z0-9_]`, or the file is missing, unreadable, not - /// UTF-8, or holds no usable row. Lines that are not JSON objects, or - /// lack a string `theorem` or `goal`, are counted rather than fatal. + /// The key fails [`validate_corpus_key`], or the file is missing, + /// unreadable, not UTF-8, or holds no usable row. Invalid rows are + /// counted and skipped rather than causing an error individually. pub fn load(training_dir: &Path, key: &str) -> Result { validate_corpus_key(key)?; let path = training_dir.join(format!("proof_states_{key}.jsonl")); @@ -371,6 +387,11 @@ impl Corpus { Ok(corpus) } + /// Look up the canonical key for an index into `entries`. + /// + /// # Panics + /// + /// Panics if `i` is outside `entries`. fn key_of(&self, i: usize) -> &StructuralKey { &self.keys[self.entries[i].key] } @@ -381,7 +402,9 @@ impl Corpus { } /// How much of the corpus the canonicaliser keyed at each tier, and how - /// often distinct statements share one structural key. + /// often distinct statements share one structural key. Tier counts + /// count `(name, statement)` rows; collisions count distinct statement + /// texts among complete structural keys only. pub fn coverage(&self) -> Coverage { let mut tiers = TierCounts::default(); for e in &self.entries { @@ -419,6 +442,7 @@ impl Corpus { } } + /// Count distinct statement texts at these entry indices, regardless of name. fn distinct_statements(&self, group: &[usize]) -> usize { group .iter() @@ -427,10 +451,12 @@ impl Corpus { .len() } - /// Sample structural keys that distinct statements share: half the - /// sample from the largest groups (trivial shapes), half from groups of - /// exactly two (where a false merge is easiest to read). Each group lists - /// at most six members. + /// Sample at most `limit` complete structural keys shared by distinct + /// statements. Take up to `limit / 2` from the largest groups (trivial + /// shapes), then fill remaining places from groups of exactly two + /// (where a false merge is easiest to read), without repeating a key. + /// Each group lists at most six distinct statements. The result may be + /// shorter than `limit` if too few eligible groups remain. pub fn collisions(&self, limit: usize) -> Vec { let mut multi: Vec<(&String, &Vec, usize)> = self .by_shape @@ -608,6 +634,7 @@ pub struct CandidateCounts { } impl CandidateCounts { + /// Count one emitted candidate in its classification. fn add(&mut self, c: Candidate) { match c { Candidate::CognateExact => self.cognate_exact += 1, @@ -618,6 +645,7 @@ impl CandidateCounts { } } + /// Count candidates across all classifications, including `unparsed`. pub fn total(&self) -> usize { self.cognate_exact + self.cognate_shape @@ -638,6 +666,7 @@ pub struct JoinCounts { } impl JoinCounts { + /// Count one candidate under the join that emitted it and its classification. fn add(&mut self, join: Join, c: Candidate) { match join { Join::NameExact => self.name_exact.add(c), @@ -689,6 +718,8 @@ pub struct ScanOptions { } impl Default for ScanOptions { + /// Skip generic name joins; cap name cross products at 64 pairs and + /// text, shape and skeleton groups at eight entries per corpus. fn default() -> Self { ScanOptions { keep_generic: false, @@ -698,6 +729,7 @@ impl Default for ScanOptions { } } +/// Distinct shape atoms for similarity, excluding `PI` and numbered variables. fn atoms(shape: &str) -> BTreeSet<&str> { shape .split(|c: char| c.is_whitespace() || matches!(c, '(' | ')' | '[' | ']')) @@ -744,6 +776,8 @@ pub fn informative(skeleton: &str) -> bool { !variable_head && constants.len() >= 3 && beyond_types } +/// Jaccard similarity of the shapes' non-variable atoms in thousandths, +/// rounded down. Return zero when both atom sets are empty. fn similarity_permille(a: &str, b: &str) -> u32 { let (sa, sb) = (atoms(a), atoms(b)); let union = sa.union(&sb).count(); @@ -753,6 +787,9 @@ fn similarity_permille(a: &str, b: &str) -> u32 { (sa.intersection(&sb).count() * 1000 / union) as u32 } +/// Prefer identical text, then matching structural and skeleton keys. +/// Differing texts with either key incomplete are `Unparsed` regardless +/// of key equality; complete statements with no match are `Differs`. fn classify(a: &Entry, ka: &StructuralKey, b: &Entry, kb: &StructuralKey) -> Candidate { if a.statement == b.statement { return Candidate::CognateExact; @@ -783,7 +820,13 @@ struct IdPair<'s> { b: IdSide<'s>, } -/// The order-independent content id of a statement pair. +/// The order-independent UUIDv8 content id of a statement pair. Each tuple +/// contains the corpus key, theorem name and statement text, used verbatim +/// without name folding or whitespace normalisation. +/// +/// # Errors +/// +/// Propagates errors from JCS serialisation in [`crate::ids::content_id`]. pub fn pair_id( (ca, na, sa): (&str, &str, &str), (cb, nb, sb): (&str, &str, &str), @@ -806,6 +849,7 @@ pub fn pair_id( Ok(crate::ids::content_id(&pair)?.to_string()) } +/// Copy an indexed corpus entry and its canonicalisation status into a candidate side. fn side(c: &Corpus, i: usize) -> Side { let e = &c.entries[i]; let k = c.key_of(i); @@ -819,6 +863,12 @@ fn side(c: &Corpus, i: usize) -> Side { } } +/// Build a candidate for the indexed entries with the supplied join and +/// classification, atom similarity and `None` evidence. +/// +/// # Errors +/// +/// Propagates content-id serialisation errors from [`pair_id`]. fn record( a: &Corpus, ia: usize, @@ -848,11 +898,19 @@ fn record( /// Scan one corpus pair, passing every candidate to `emit` in a fixed /// order: name joins by folded name, then text, shape and skeleton joins, -/// each by key. A pair is reported by the first join that finds it. +/// each by key. Later joins exclude pairs meeting an earlier join +/// criterion, even if that earlier group was skipped by a limit. Limits +/// skip whole groups rather than truncating them. Shape and skeleton +/// joins require complete keys and an [`informative`] skeleton; text joins +/// require at least three whitespace-separated tokens. +/// +/// Return candidate counts and skipped-group counts. Every emitted record +/// carries `None` evidence. /// /// # Errors /// -/// Whatever `emit` returns, or a failure to derive a content id. +/// Propagates errors from `emit` or content-id serialisation, stopping at +/// the first error. Earlier callback side effects are not rolled back. pub fn scan_pair( a: &Corpus, b: &Corpus, @@ -1010,6 +1068,10 @@ pub fn scan_pair( } /// Serialise `value` as one JCS line (RFC 8785 plus a final LF). +/// +/// # Errors +/// +/// Propagates errors from JSON serialisation or JCS canonicalisation. pub fn jcs_line(value: &T) -> Result> { let mut bytes = serde_json_canonicalizer::to_vec(value)?; bytes.push(b'\n'); @@ -1038,6 +1100,13 @@ pub struct RunReport { pub total: Duration, } +/// Create or truncate `path`, write each item as a JCS line, then flush. +/// Parent directories must already exist; an empty slice creates an empty file. +/// +/// # Errors +/// +/// Propagates file creation, serialisation, write and flush errors. A +/// failure may leave the file empty or partially written. fn write_lines(path: &Path, items: &[T]) -> Result<()> { let mut w = BufWriter::new(File::create(path).with_context(|| format!("create {}", path.display()))?); @@ -1050,11 +1119,19 @@ fn write_lines(path: &Path, items: &[T]) -> Result<()> { /// Load every corpus the pairs name (each once), scan each pair, and write /// `pairs/__.jsonl`, `summary.jsonl`, `coverage.jsonl` and -/// `collisions/.jsonl` under `opts.out`. +/// `collisions/.jsonl` under `opts.out`. Return coverage, pair +/// summaries and timings; timings are omitted from the files. +/// +/// Create output directories as needed, remove existing `.jsonl` files +/// directly inside `pairs/` and `collisions/`, and replace the coverage +/// and summary files. Pairs are scanned in the supplied order. /// /// # Errors /// -/// A corpus fails to load, or an output file cannot be written. +/// No pairs are supplied, a corpus fails to load, output directories +/// cannot be created or read, an old file cannot be removed, or +/// serialisation, file creation, writing or flushing fails. Output may +/// already have been removed or partially written when an error occurs. pub fn run(opts: &RunOptions) -> Result { let started = Instant::now(); if opts.pairs.is_empty() { diff --git a/src/rust/main.rs b/src/rust/main.rs index 68a033d6..fd3100c7 100644 --- a/src/rust/main.rs +++ b/src/rust/main.rs @@ -452,6 +452,7 @@ enum DesignOp { }, } +/// Run the selected CLI command after configuring tracing, colours and output. #[tokio::main] async fn main() -> Result<()> { // Parse CLI arguments @@ -1377,7 +1378,10 @@ async fn diagnostics_command() -> Result<()> { /// # Errors /// /// An unknown preset, a malformed `--pair`, no pairs at all, a corpus that -/// fails to load, or an output file that cannot be written. +/// fails to load, an output directory that cannot be created or read, an +/// old output file that cannot be removed, or a serialisation or output +/// write failure. Also returns an error if the scan thread cannot be +/// spawned or panics. Failed scans may leave partial output. fn lexicon_command(op: LexiconOp) -> Result<()> { use echidna::lexicon::scan::{self, RunOptions, ScanOptions}; @@ -1505,6 +1509,8 @@ fn lexicon_command(op: LexiconOp) -> Result<()> { /// /// Crossquery prints exact semantic-class and canonical-name matches from /// per-prover tables and, unless `provers_only` is set, cross-prover dictionaries. +/// Identity queries skip declarations whose canonical keys are incomplete +/// and report the number skipped; only complete keys form identity groups. /// /// # Errors /// From 4b8a4c8ecd60996f28a686ad52334b8757c399bd Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 27 Oct 2026 05:26:10 +0000 Subject: [PATCH 11/16] fix(corpus,lexicon): mismatched closers and unterminated quotes or comments are incomplete; keep line breaks; clean up only generated files - `complete` is false when a closer meets a group of another kind, or a quoted statement or block comment runs off the end. A closer with no group open stays the parser's call, so ACL2's trailing `defthm` closer is still accepted. - Whitespace runs collapse to a newline when they hold one, so a line comment no longer swallows the rest of a statement. - A re-run removes only `pairs/__.jsonl` and `collisions/.jsonl` names, not every `.jsonl`. - ADR coverage table and totals refreshed from a full rescan. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01WS4mfQeC3N1DWjcCQJaQqw --- CHANGELOG.adoc | 7 +- docs/CORPUS.adoc | 8 +- ...9-lexicon-v2-and-identity-arbitration.adoc | 36 ++++---- src/rust/corpus/canonical.rs | 64 +++++++++++++- src/rust/lexicon/scan.rs | 88 ++++++++++++++++--- 5 files changed, 168 insertions(+), 35 deletions(-) diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index a2c48ba8..b04d4352 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -19,6 +19,9 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning]. `+data/synonyms/+` is never written. Presets `+learning+`, `+spanning+` (one corpus per prover family), `+in-family+` and `+full+`. Per-corpus coverage and key-collision samples are written alongside. + Whitespace runs collapse to one space, or to a newline when they hold + one, so a line comment cannot swallow the rest of a statement. A re-run + removes only the file names the scan writes. ==== Fixed — canonicaliser, 2026-10-27 @@ -28,7 +31,9 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning]. and the octad identity keys. No key changes. * *`+StructuralKey::complete+`* (new, `+#[serde(default)]+`) reports whether the shape accounts for the whole statement: false when the - parser stops early or the input ends inside an open bracket, meets + parser stops early, invents a missing operand, or the input ends inside + an open bracket, a quoted statement or a block comment; when a closer + meets a group of another kind; when the statement meets notation `+dk-shape-v1+` has no rule for (HOL binders, `+~+`, `+==>+`, Isabelle `+\<…>+` escapes), drops a statement's own leading tokens as a "header", misreads a leading group as a telescope, or cuts off nesting diff --git a/docs/CORPUS.adoc b/docs/CORPUS.adoc index b54c5d01..725f739a 100644 --- a/docs/CORPUS.adoc +++ b/docs/CORPUS.adoc @@ -244,9 +244,11 @@ consumer that only compares one field should compare both. A key is only as good as the parse behind it. `+StructuralKey::complete+` says whether the canonicaliser read the *whole* statement; when it did not -(its parser stopped early, it met notation it has no rule for — HOL's `+!+` -and `+?+` binders, Isabelle's `+\<…>+` escapes — or a header drop discarded -the statement's own leading tokens), the key is still reported at the +(its parser stopped early or invented an operand, the input ended inside an +open bracket, quote or comment, a closer met a group of another kind, it +met notation it has no rule for — HOL's `+!+` and `+?+` binders, Isabelle's +`+\<…>+` escapes — or a header drop discarded the statement's own leading +tokens), the key is still reported at the structural tier but is a *prefix* that other statements share. Treat an incomplete key as no identity at all: `+corpus identity+` skips such declarations and reports how many it skipped. Measured on `+training_data/+`, the diff --git a/docs/decisions/2026-10-19-lexicon-v2-and-identity-arbitration.adoc b/docs/decisions/2026-10-19-lexicon-v2-and-identity-arbitration.adoc index a0a03c2b..87d3bd65 100644 --- a/docs/decisions/2026-10-19-lexicon-v2-and-identity-arbitration.adoc +++ b/docs/decisions/2026-10-19-lexicon-v2-and-identity-arbitration.adoc @@ -336,6 +336,8 @@ share that prefix. `StructuralKey::complete` now says whether the whole statement was read. It is false when the parser stops early, invents a missing operand (`x + 1 =`) or reaches the end inside an open bracket or an unclosed `(assert …` wrapper (ACL2s goals truncated mid-expression), +when a closer meets a group of another kind (`(x]`) or a quoted statement +or block comment never closes, when the statement holds notation the scheme has no rule for (`!`, `?`, `@` and `\` binders, `~`, `==>`, Isabelle's `\<…>` escapes, Lean 3's `$`; checked before binders and ascriptions are removed), when a header drop @@ -349,19 +351,19 @@ Share of each corpus read completely (`dk-shape-v1`, 2026-10-27): [cols="2,2,2,2,2",options="header"] |=== | Corpus | Distinct rows | Read completely | Keys shared by distinct statements | Homonymous names -| acl2 | 135963 | 16.1 % | 798 | 8.0 % -| acl2s | 112677 | 5.3 % | 352 | 4.8 % -| afp | 102683 | 10.7 % | 522 | 2.1 % -| agda | 46028 | 41.0 % | 578 | 8.6 % -| dafny | 10487 | 53.8 % | 154 | 12.2 % -| dedukti | 1453 | 76.0 % | 54 | 20.6 % -| hol4 | 95738 | 8.7 % | 107 | 4.2 % +| acl2 | 135963 | 16.0 % | 783 | 8.0 % +| acl2s | 112742 | 4.8 % | 330 | 4.8 % +| afp | 102717 | 10.7 % | 530 | 2.1 % +| agda | 46028 | 40.9 % | 577 | 8.6 % +| dafny | 10487 | 53.8 % | 153 | 12.2 % +| dedukti | 1453 | 75.4 % | 54 | 20.6 % +| hol4 | 95738 | 8.6 % | 106 | 4.2 % | hol_light | 43937 | 1.9 % | 15 | 2.9 % | isabelle_zf | 3577 | 0.4 % | 0 | 0.3 % -| lambda_prolog | 24897 | 93.6 % | 122 | 50.0 % -| lean3 | 92680 | 26.5 % | 2777 | 19.2 % -| mizar | 76522 | 20.0 % | 477 | 1.8 % -| why3 | 25180 | 28.5 % | 378 | 21.9 % +| lambda_prolog | 24897 | 93.5 % | 120 | 50.0 % +| lean3 | 92695 | 26.0 % | 2675 | 19.2 % +| mizar | 76522 | 19.5 % | 456 | 1.8 % +| why3 | 25180 | 28.2 % | 365 | 21.9 % |=== "Keys shared by distinct statements" counts complete keys only. Most are @@ -404,11 +406,11 @@ identity keys (E6 `cross_prover_identity_key`) inherit all four causes. === What the measurement found in the corpora -Over all 33 pairs: 203,860 same-name statement pairs, of which 1,070 are -exact cognates, 2,708 shape cognates, 71 skeleton (specialisation) -candidates, 7,854 differ, and 192,157 (94 %) are `unparsed`. Synonym -candidates under different names: 315 by identical text, 491 by shape, -865 by skeleton. Debug build: 179 s for all thirteen corpora, almost all +Over all 33 pairs: 204,002 same-name statement pairs, of which 1,070 are +exact cognates, 2,631 shape cognates, 69 skeleton (specialisation) +candidates, 7,512 differ, and 192,720 (94 %) are `unparsed`. Synonym +candidates under different names: 315 by identical text, 436 by shape, +822 by skeleton. Debug build: 168 s for all thirteen corpora, almost all of it loading and canonicalising; one pair scans in about a second. * *HOL4 ↔ HOL Light* (pilot pair): 1,033 exact cognates and 144 text @@ -429,7 +431,7 @@ of it loading and canonicalising; one pair scans in about a second. short-name rule above), fewer than three constants, or a bare type signature (λProlog's `int -> int -> int` against Dedukti's `Int -> Int -> Int`) say nothing about which statement it is. Joins - between different names skip them (3,335 groups, counted). + between different names skip them (3,295 groups, counted). === Equivalence by invariant and by witness diff --git a/src/rust/corpus/canonical.rs b/src/rust/corpus/canonical.rs index 441efe3e..3c11fcaf 100644 --- a/src/rust/corpus/canonical.rs +++ b/src/rust/corpus/canonical.rs @@ -303,6 +303,13 @@ fn is_ident_char(c: char) -> bool { } fn lex(src: &str) -> Vec { + lex_flagged(src).0 +} + +/// Lex `src`; the flag is false when a quoted statement or block comment +/// runs off the end of the input (part of the statement was swallowed). +fn lex_flagged(src: &str) -> (Vec, bool) { + let mut terminated = true; let chars: Vec = src.chars().collect(); let n = chars.len(); let mut out: Vec = Vec::new(); @@ -328,6 +335,9 @@ fn lex(src: &str) -> Vec { while i + 1 < n && !(chars[i] == '*' && chars[i + 1] == ')') { i += 1; } + if i + 1 >= n { + terminated = false; + } i = (i + 2).min(n); continue; } @@ -338,7 +348,12 @@ fn lex(src: &str) -> Vec { j += 1; } let inner: String = chars[i + 1..j.min(n)].iter().collect(); - out.extend(lex(&inner)); + if j >= n { + terminated = false; + } + let (inner_toks, inner_ok) = lex_flagged(&inner); + terminated &= inner_ok; + out.extend(inner_toks); i = j + 1; continue; } @@ -392,7 +407,36 @@ fn lex(src: &str) -> Vec { out.push(Tk::Sym(c.to_string())); i += 1; } - out + (out, terminated) +} + +/// True when every closer that meets an open group is of that group's kind +/// and nothing is left open. A mismatched closer (`(x]`) is not a structure +/// the parser can read faithfully. A closer with no group open is left to +/// the parser: extraction often keeps the enclosing form's closer at the +/// end (ACL2 `defthm … )`), which `rest_is_ignorable` accepts, while a +/// stray closer followed by more of the statement stops the parse early. +fn brackets_balanced(toks: &[Tk]) -> bool { + let mut stack: Vec = Vec::new(); + for t in toks { + match t { + Tk::Open(c) => stack.push(*c), + Tk::Close(c) => { + let want = match c { + ')' => '(', + ']' => '[', + _ => '{', + }; + match stack.pop() { + None => {}, + Some(open) if open == want => {}, + Some(_) => return false, + } + }, + _ => {}, + } + } + stack.is_empty() } // =========================================================================== @@ -1253,7 +1297,12 @@ fn has_unread_notation(body: &[Tk]) -> bool { /// as a telescope, the body holds no unread notation, and the parser /// consumed the body. fn normalise(statement: &str) -> (String, String, bool) { - let (toks, dropped_body) = strip_header(&lex(statement)); + let (raw, terminated) = lex_flagged(statement); + // Read over the whole statement, header included: a mismatched or + // stray bracket, or a quote or block comment that never closes, means + // the tokens are not the statement as written. + let well_formed = terminated && brackets_balanced(&raw); + let (toks, dropped_body) = strip_header(&raw); // Checked before ascriptions and binders are removed: a binder's sort // can hold notation too (`(x : F $ A)`), and extraction would drop it. let unread = has_unread_notation(&toks); @@ -1263,6 +1312,7 @@ fn normalise(statement: &str) -> (String, String, bool) { let mut parser = Parser::new(body, varmap); let ast = parser.expr(0); let complete = !has_hole(&ast) + && well_formed && parser.rest_is_ignorable() && parser.unclosed == 0 && !parser.too_deep @@ -1509,6 +1559,8 @@ mod tests { assert!(k.complete, "{prover}: {s:?} -> {}", k.shape); } assert!(structural_key("Lemma add_comm : forall x y : nat, x + y = y + x.").complete); + // ACL2 extraction keeps the `defthm` form's closer at the end + assert!(structural_key("(equal (len (rev x)) (len x)))").complete); } /// Statements the scheme cannot read are marked incomplete even though @@ -1533,6 +1585,12 @@ mod tests { // change) and reported "(assert x y", "(assert (forall ((x Nat)) (= x x", + // a closer of the wrong kind, or a stray one + "(x + y] = z", + "x + y) = z", + // a quote or block comment that runs off the end + "\"x + y = y + x", + "x + y = y + x (* commutes", // notation inside a binder's sort is dropped by extraction "forall (x : F $ A), x + 0 = x", // Isabelle ASCII symbol escapes diff --git a/src/rust/lexicon/scan.rs b/src/rust/lexicon/scan.rs index cfbc0a31..cd945d8b 100644 --- a/src/rust/lexicon/scan.rs +++ b/src/rust/lexicon/scan.rs @@ -244,8 +244,57 @@ pub struct Corpus { by_skeleton: BTreeMap>, } +/// Collapse each whitespace run to one character: a newline if the run +/// holds one, else a space. Line breaks are kept because they end line +/// comments (`-- …`, `// …`); joining the lines would turn the rest of +/// the statement into comment. fn collapse_whitespace(s: &str) -> String { - s.split_whitespace().collect::>().join(" ") + let mut out = String::with_capacity(s.len()); + let mut pending: Option = None; + for c in s.trim().chars() { + if c.is_whitespace() { + if c == '\n' { + pending = Some('\n'); + } else if pending.is_none() { + pending = Some(' '); + } + } else { + if let Some(p) = pending.take() { + out.push(p); + } + out.push(c); + } + } + out +} + +/// `__.jsonl` with two valid corpus keys: a name `run` writes. +fn is_pair_file_name(name: &str) -> bool { + name.strip_suffix(".jsonl") + .and_then(|stem| stem.split_once("__")) + .is_some_and(|(a, b)| validate_corpus_key(a).is_ok() && validate_corpus_key(b).is_ok()) +} + +/// Remove the files in `dir` whose names `is_ours` recognises. +fn remove_generated(dir: &Path, is_ours: fn(&str) -> bool) -> Result<()> { + for entry in fs::read_dir(dir).with_context(|| format!("read {}", dir.display()))? { + let path = entry?.path(); + let ours = path.is_file() + && path + .file_name() + .and_then(|n| n.to_str()) + .is_some_and(is_ours); + if ours { + fs::remove_file(&path).with_context(|| format!("remove {}", path.display()))?; + } + } + Ok(()) +} + +/// `.jsonl` with a valid corpus key: a name `run` writes. +fn is_collision_file_name(name: &str) -> bool { + name.strip_suffix(".jsonl") + .is_some_and(|stem| validate_corpus_key(stem).is_ok()) } impl Corpus { @@ -1081,16 +1130,11 @@ pub fn run(opts: &RunOptions) -> Result { fs::create_dir_all(&collisions_dir) .with_context(|| format!("create {}", collisions_dir.display()))?; // A re-run over a different pair set must not leave the previous run's - // files beside this run's summary. Only the scan's own `.jsonl` files - // are removed; anything else in the directory is left alone. - for dir in [&pairs_dir, &collisions_dir] { - for entry in fs::read_dir(dir).with_context(|| format!("read {}", dir.display()))? { - let path = entry?.path(); - if path.extension().and_then(|e| e.to_str()) == Some("jsonl") { - fs::remove_file(&path).with_context(|| format!("remove {}", path.display()))?; - } - } - } + // files beside this run's summary. Only names this command writes are + // removed (`pairs/__.jsonl` and `collisions/.jsonl`, with + // valid corpus keys); anything else in the directory is left alone. + remove_generated(&pairs_dir, is_pair_file_name)?; + remove_generated(&collisions_dir, is_collision_file_name)?; let coverage: Vec = corpora.values().map(Corpus::coverage).collect(); write_lines(&opts.out.join("coverage.jsonl"), &coverage)?; @@ -1226,6 +1270,28 @@ mod tests { assert!(canonical::token_count("x = y") >= 3); } + #[test] + fn collapsing_whitespace_keeps_the_line_break_that_ends_a_comment() { + let s = "x = y -- note\n \t /\\ y = x "; + assert_eq!(collapse_whitespace(s), "x = y -- note\n/\\ y = x"); + assert_eq!(collapse_whitespace("a \t b"), "a b"); + // the conjunct after the comment still reaches the canonicaliser + let joined = canonical::structural_key(&collapse_whitespace(s)); + let split = canonical::structural_key("x = y /\\ y = x"); + assert_eq!(joined.shape, split.shape); + } + + #[test] + fn cleanup_matches_only_generated_names() { + assert!(is_pair_file_name("hol4__hol_light.jsonl")); + assert!(!is_pair_file_name("notes.jsonl")); + assert!(!is_pair_file_name("hol4__Hol.jsonl")); + assert!(!is_pair_file_name("hol4__hol_light.json")); + assert!(is_collision_file_name("lean3.jsonl")); + assert!(!is_collision_file_name("my-export.jsonl")); + assert!(!is_collision_file_name("lean3.txt")); + } + #[test] fn pair_ids_ignore_side_order() { let x = ("hol4", "ADD_COMM", "!m n. m + n = n + m"); From 1a8dc36bcf591a316d0d042ad2136c53e3f85852 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 27 Oct 2026 05:42:04 +0000 Subject: [PATCH 12/16] fix(corpus): string literals are opaque atoms, not re-lexed formulas A quoted span is lexed as a formula only where it wraps one (start of statement, after `:`, after an Isabelle statement keyword). Elsewhere it is a single constant, so `s = "a//b"` and `s = "a//c"` no longer lose their tails to a `//` comment and share a key. Backslash escapes the next character. Statements with such literals get new keys; ADR numbers refreshed from a full rescan. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01WS4mfQeC3N1DWjcCQJaQqw --- CHANGELOG.adoc | 9 +++ ...9-lexicon-v2-and-identity-arbitration.adoc | 20 +++--- src/rust/corpus/canonical.rs | 70 +++++++++++++++++-- 3 files changed, 84 insertions(+), 15 deletions(-) diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index b04d4352..967ce331 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -29,6 +29,15 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning]. token is an unbalanced opening bracket (eight `+open + 1..close+` slices are now guarded). `+structural_key+` reaches this from `+corpus ingest+` and the octad identity keys. No key changes. +* *String literals are opaque atoms.* A quoted span is lexed as a formula + only where it wraps one: at the start of a statement, after `+:+`, or + after an Isabelle statement keyword. Elsewhere (`+s = "a//b"+`, ACL2 + `+"Goal"+` hints, Why3 `+meta "…"+`) it is one constant, so its contents + are no longer read as comments, operators or variables, and a backslash + escapes the next character. *Key change*: statements with such a literal + get new keys; distinct literals no longer share one. On + `+training_data/+` this splits a dozen Mizar and seven Why3 key + collisions; coverage moves by at most 0.1 point per corpus. * *`+StructuralKey::complete+`* (new, `+#[serde(default)]+`) reports whether the shape accounts for the whole statement: false when the parser stops early, invents a missing operand, or the input ends inside diff --git a/docs/decisions/2026-10-19-lexicon-v2-and-identity-arbitration.adoc b/docs/decisions/2026-10-19-lexicon-v2-and-identity-arbitration.adoc index 87d3bd65..dd23ac85 100644 --- a/docs/decisions/2026-10-19-lexicon-v2-and-identity-arbitration.adoc +++ b/docs/decisions/2026-10-19-lexicon-v2-and-identity-arbitration.adoc @@ -354,16 +354,16 @@ Share of each corpus read completely (`dk-shape-v1`, 2026-10-27): | acl2 | 135963 | 16.0 % | 783 | 8.0 % | acl2s | 112742 | 4.8 % | 330 | 4.8 % | afp | 102717 | 10.7 % | 530 | 2.1 % -| agda | 46028 | 40.9 % | 577 | 8.6 % +| agda | 46028 | 40.9 % | 579 | 8.6 % | dafny | 10487 | 53.8 % | 153 | 12.2 % | dedukti | 1453 | 75.4 % | 54 | 20.6 % -| hol4 | 95738 | 8.6 % | 106 | 4.2 % +| hol4 | 95738 | 8.7 % | 106 | 4.2 % | hol_light | 43937 | 1.9 % | 15 | 2.9 % | isabelle_zf | 3577 | 0.4 % | 0 | 0.3 % -| lambda_prolog | 24897 | 93.5 % | 120 | 50.0 % -| lean3 | 92695 | 26.0 % | 2675 | 19.2 % -| mizar | 76522 | 19.5 % | 456 | 1.8 % -| why3 | 25180 | 28.2 % | 365 | 21.9 % +| lambda_prolog | 24897 | 93.5 % | 119 | 50.0 % +| lean3 | 92695 | 26.0 % | 2677 | 19.2 % +| mizar | 76522 | 19.4 % | 444 | 1.8 % +| why3 | 25180 | 28.3 % | 358 | 21.9 % |=== "Keys shared by distinct statements" counts complete keys only. Most are @@ -408,9 +408,9 @@ identity keys (E6 `cross_prover_identity_key`) inherit all four causes. Over all 33 pairs: 204,002 same-name statement pairs, of which 1,070 are exact cognates, 2,631 shape cognates, 69 skeleton (specialisation) -candidates, 7,512 differ, and 192,720 (94 %) are `unparsed`. Synonym -candidates under different names: 315 by identical text, 436 by shape, -822 by skeleton. Debug build: 168 s for all thirteen corpora, almost all +candidates, 7,516 differ, and 192,716 (94 %) are `unparsed`. Synonym +candidates under different names: 315 by identical text, 433 by shape, +819 by skeleton. Debug build: 177 s for all thirteen corpora, almost all of it loading and canonicalising; one pair scans in about a second. * *HOL4 ↔ HOL Light* (pilot pair): 1,033 exact cognates and 144 text @@ -431,7 +431,7 @@ of it loading and canonicalising; one pair scans in about a second. short-name rule above), fewer than three constants, or a bare type signature (λProlog's `int -> int -> int` against Dedukti's `Int -> Int -> Int`) say nothing about which statement it is. Joins - between different names skip them (3,295 groups, counted). + between different names skip them (3,279 groups, counted). === Equivalence by invariant and by witness diff --git a/src/rust/corpus/canonical.rs b/src/rust/corpus/canonical.rs index 50fbd454..5a24fd72 100644 --- a/src/rust/corpus/canonical.rs +++ b/src/rust/corpus/canonical.rs @@ -343,19 +343,29 @@ fn lex_flagged(src: &str) -> (Vec, bool) { i = (i + 2).min(n); continue; } - // quoted statement (Isabelle quotes the whole formula) + // A quoted span is either a formula wrapper (Isabelle quotes the whole + // formula: `"x = y"`, `lemma foo: "…"`, `assumes "…" shows "…"`), + // whose contents are lexed as the statement, or a string literal + // (`s = "a//b"`, ACL2's `"Goal"` hints), which is one opaque atom so + // its contents are never read as comments, operators or variables. if c == '"' { let mut j = i + 1; while j < n && chars[j] != '"' { - j += 1; + // a backslash escapes the next character (`\"` in a literal, + // `\` in an Isabelle formula) + j += if chars[j] == '\\' { 2 } else { 1 }; } let inner: String = chars[i + 1..j.min(n)].iter().collect(); if j >= n { terminated = false; } - let (inner_toks, inner_ok) = lex_flagged(&inner); - terminated &= inner_ok; - out.extend(inner_toks); + if opens_formula(out.last()) { + let (inner_toks, inner_ok) = lex_flagged(&inner); + terminated &= inner_ok; + out.extend(inner_toks); + } else { + out.push(Tk::Name(format!("\"{inner}\""))); + } i = j + 1; continue; } @@ -412,6 +422,29 @@ fn lex_flagged(src: &str) -> (Vec, bool) { (out, terminated) } +/// Whether a quote after `prev` wraps a formula rather than a string +/// literal: at the start of the statement, after a `:` (`lemma foo: "…"`), +/// or after an Isabelle statement keyword. +fn opens_formula(prev: Option<&Tk>) -> bool { + const KEYWORDS: [&str; 9] = [ + "lemma", + "theorem", + "corollary", + "proposition", + "schematic_goal", + "assumes", + "shows", + "obtains", + "and", + ]; + match prev { + None => true, + Some(Tk::Sym(s)) => s == ":", + Some(Tk::Id(s)) => KEYWORDS.contains(&s.as_str()), + _ => false, + } +} + /// True when every closer that meets an open group is of that group's kind /// and nothing is left open. A mismatched closer (`(x]`) is not a structure /// the parser can read faithfully. A closer with no group open is left to @@ -1577,6 +1610,33 @@ mod tests { assert!(structural_key("(equal (len (rev x)) (len x)))").complete); } + /// A string literal is one opaque atom; a formula wrapper is unwrapped. + #[test] + fn string_literals_are_atoms_and_formula_quotes_are_unwrapped() { + let a = structural_key("s = \"a//b\""); + let b = structural_key("s = \"a//c\""); + assert!(a.complete && b.complete); + assert_ne!(a.key, b.key, "the literal's tail is not a comment"); + assert_ne!( + structural_key("s = \"x\"").key, + structural_key("s = x").key, + "a literal is not the variable it spells" + ); + assert_ne!( + structural_key("s = \"a \\\" b\"").key, + structural_key("s = \"a \\\" c\"").key, + "an escaped quote does not end the literal" + ); + let bare = structural_key("x + y = y + x").key; + for s in ["\"x + y = y + x\"", "lemma add_comm: \"x + y = y + x\""] { + assert_eq!(structural_key(s).key, bare, "{s}"); + } + // An anonymous `lemma "…"` loses its first token to the header drop + // (a dk-shape-v1 rule, D6); the drop is reported, never trusted. + let anon = structural_key("lemma \"x + y = y + x\""); + assert!(anon.key == bare || !anon.complete); + } + /// Statements the scheme cannot read are marked incomplete even though /// they still get a structural-tier key. #[test] From 3a9fbf0e9558b556884e86e683b03d801314fc44 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 27 Oct 2026 05:52:26 +0000 Subject: [PATCH 13/16] fix(corpus,lexicon): bound operator chains, restore dk-shape-v1 ascription rule, cap folded groups, unambiguous pair names MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - The parser counts infix-operator nesting against MAX_NESTING as well as brackets: a 200k-operator `a -> a -> …` chain overflowed the stack; it is now cut off and marked incomplete. - drop_ascriptions is linear again without changing dk-shape-v1: bracket matches and identifier/symbol counts are precomputed, so `(f 0 :: nat)` and `((x) :: nat)` reduce as before. A proptest checks it against the shipped implementation. - The per-name cap bounds folded-name pairs across a whole folded group, not per raw-name pair. - Corpus keys may not start or end with `_` (`a_:b` and `a:_b` both wrote pairs/a___b.jsonl). - ADR totals refreshed from a full rescan. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01WS4mfQeC3N1DWjcCQJaQqw --- CHANGELOG.adoc | 12 +- ...9-lexicon-v2-and-identity-arbitration.adoc | 12 +- src/rust/corpus/canonical.rs | 213 +++++++++++++++--- src/rust/lexicon/scan.rs | 95 +++++++- src/rust/main.rs | 3 +- 5 files changed, 279 insertions(+), 56 deletions(-) diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index 967ce331..57e2779a 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -22,6 +22,9 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning]. Whitespace runs collapse to one space, or to a newline when they hold one, so a line comment cannot swallow the rest of a statement. A re-run removes only the file names the scan writes. + The per-name cap (`+--max-pairs-per-name+`) bounds folded-name pairs + across a whole folded group, not per raw-name pair. Corpus keys may not + start or end with `+_+`, so pair file names stay unambiguous. ==== Fixed — canonicaliser, 2026-10-27 @@ -45,10 +48,11 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning]. meets a group of another kind; when the statement meets notation `+dk-shape-v1+` has no rule for (HOL binders, `+~+`, `+==>+`, Isabelle `+\<…>+` escapes), drops a statement's own leading tokens as a - "header", misreads a leading group as a telescope, or cuts off nesting - deeper than 256 levels (the parser is now bounded, so a deeply nested - statement cannot overflow a caller's stack). `+corpus identity+` skips - incomplete declarations and says how many. No key changes. + "header", misreads a leading group as a telescope, or cuts off a tree + deeper than 256 levels, counting bracket groups and infix operators + (the parser is now bounded, so neither deep nesting nor a long flat + chain such as `+a -> a -> …+` can overflow a caller's stack). + `+corpus identity+` skips incomplete declarations and says how many. No key changes. Measured on `+training_data/+`, 0.4 %–94 % of a corpus is read completely; the rule-level causes are recorded for a `+dk-shape-v2+` decision in `+docs/decisions/2026-10-19-lexicon-v2-and-identity-arbitration.adoc+`. diff --git a/docs/decisions/2026-10-19-lexicon-v2-and-identity-arbitration.adoc b/docs/decisions/2026-10-19-lexicon-v2-and-identity-arbitration.adoc index dd23ac85..62af8d3a 100644 --- a/docs/decisions/2026-10-19-lexicon-v2-and-identity-arbitration.adoc +++ b/docs/decisions/2026-10-19-lexicon-v2-and-identity-arbitration.adoc @@ -406,11 +406,13 @@ identity keys (E6 `cross_prover_identity_key`) inherit all four causes. === What the measurement found in the corpora -Over all 33 pairs: 204,002 same-name statement pairs, of which 1,070 are -exact cognates, 2,631 shape cognates, 69 skeleton (specialisation) -candidates, 7,516 differ, and 192,716 (94 %) are `unparsed`. Synonym -candidates under different names: 315 by identical text, 433 by shape, -819 by skeleton. Debug build: 177 s for all thirteen corpora, almost all +Over all 33 pairs: 167,040 same-name statement pairs, of which 1,070 are +exact cognates, 2,631 shape cognates, 64 skeleton (specialisation) +candidates, 5,777 differ, and 157,498 (94 %) are `unparsed`. A further +90,191 statement pairs under 308 over-large names are counted, not +emitted: the per-name cap (64) bounds exact pairs per raw name and folded +pairs per folded name. Synonym candidates under different names: 315 by +identical text, 433 by shape, 819 by skeleton. Debug build: 167 s for all thirteen corpora, almost all of it loading and canonicalising; one pair scans in about a second. * *HOL4 ↔ HOL Light* (pilot pair): 1,033 exact cognates and 144 text diff --git a/src/rust/corpus/canonical.rs b/src/rust/corpus/canonical.rs index 5a24fd72..da26756d 100644 --- a/src/rust/corpus/canonical.rs +++ b/src/rust/corpus/canonical.rs @@ -929,40 +929,72 @@ fn extract_binders(toks: &[Tk]) -> (Vec, Binders) { /// Unwrap Isabelle-style `(x :: nat)` ascriptions with recognised sorts, /// retaining the term identifier. Other groups are preserved. +/// +/// A group qualifies when, between its brackets, there are exactly two +/// identifiers and one symbol, the symbol is `::` and the second identifier +/// is a known sort; numbers and nested brackets do not count. The group is +/// replaced by the first identifier, so `(f 0 :: nat)` and `((x) :: nat)` +/// reduce as `dk-shape-v1` always has. Bracket matches and token counts are +/// computed once, so the pass is linear even on deeply nested input. fn drop_ascriptions(toks: &[Tk]) -> Vec { + let n = toks.len(); + // close[i]: the index `matching(toks, i)` returns for an opener at `i`. + let mut close: Vec = vec![n.saturating_sub(1); n]; + let mut stack: Vec = Vec::new(); + for (j, t) in toks.iter().enumerate() { + if is_open(t) { + stack.push(j); + } else if is_close(t) { + if let Some(i) = stack.pop() { + close[i] = j; + } + } + } + // Prefix counts and next-occurrence tables for identifiers and symbols. + let mut ids_before = vec![0usize; n + 1]; + let mut syms_before = vec![0usize; n + 1]; + for (k, t) in toks.iter().enumerate() { + ids_before[k + 1] = ids_before[k] + usize::from(matches!(t, Tk::Id(_))); + syms_before[k + 1] = syms_before[k] + usize::from(matches!(t, Tk::Sym(_))); + } + let mut next_id = vec![n; n + 1]; + let mut next_sym = vec![n; n + 1]; + for k in (0..n).rev() { + next_id[k] = if matches!(toks[k], Tk::Id(_)) { + k + } else { + next_id[k + 1] + }; + next_sym[k] = if matches!(toks[k], Tk::Sym(_)) { + k + } else { + next_sym[k + 1] + }; + } + let id_at = |k: usize| match &toks[k] { + Tk::Id(s) => s, + _ => unreachable!("next_id points at an identifier"), + }; + let mut out: Vec = Vec::new(); let mut i = 0usize; - while i < toks.len() { + while i < n { if is_open(&toks[i]) { - // Only `( x :: sort )` qualifies, so a group without `::` in second - // place is left alone without scanning for its close (that scan - // made this quadratic on deeply nested input). - let could_ascribe = matches!(toks.get(i + 2), Some(Tk::Sym(s)) if s == "::"); - if !could_ascribe { - out.push(toks[i].clone()); - i += 1; - continue; - } - let j = matching(toks, i); - let inner: Vec = between(toks, i, j).to_vec(); - let ids: Vec<&String> = inner - .iter() - .filter_map(|t| match t { - Tk::Id(s) => Some(s), - _ => None, - }) - .collect(); - let syms: Vec<&String> = inner - .iter() - .filter_map(|t| match t { - Tk::Sym(s) => Some(s), - _ => None, - }) - .collect(); - if ids.len() == 2 && syms.len() == 1 && syms[0] == "::" && sort_of(ids[1]).is_some() { - out.push(Tk::Id(ids[0].clone())); - i = j + 1; - continue; + let j = close[i]; + // the tokens strictly between, as `between(toks, i, j)` gives them + let (lo, hi) = (i + 1, j.max(i + 1)); + let ids = ids_before[hi] - ids_before[lo]; + let syms = syms_before[hi] - syms_before[lo]; + if ids == 2 && syms == 1 { + let first = next_id[lo]; + let second = next_id[first + 1]; + let is_ascription = matches!(&toks[next_sym[lo]], Tk::Sym(s) if s == "::") + && sort_of(id_at(second)).is_some(); + if is_ascription { + out.push(Tk::Id(id_at(first).clone())); + i = j + 1; + continue; + } } } out.push(toks[i].clone()); @@ -994,17 +1026,22 @@ struct Parser { /// truncated inside a group (`(x = y`) parses to the end and would /// otherwise look complete. unclosed: usize, - /// Current bracket nesting, bounded by [`MAX_NESTING`]. + /// Current tree depth (brackets and operator nesting), bounded by + /// [`MAX_NESTING`]. depth: usize, - /// A group deeper than [`MAX_NESTING`] was skipped as a hole. + /// The tree reached [`MAX_NESTING`]: a group was skipped as a hole, or + /// the rest of an operator chain was skipped. too_deep: bool, } -/// Deepest bracket nesting the parser descends into. Each level costs three -/// stack frames (`expr` → `app` → `atom`), and `structural_key` runs on the -/// caller's stack (`corpus ingest`, octad export), so a statement nested -/// deeper than this is cut off rather than allowed to overflow it. The -/// shipped corpora reach a depth in the fifties. +/// Deepest tree the parser builds. Each bracket group and each infix +/// operator nests the tree one level (a bracket costs three stack frames, +/// `expr` → `app` → `atom`; a right-associative operator costs one `expr` +/// frame; a left-associative chain deepens the tree that `render`, +/// `has_hole` and drop then walk). `structural_key` runs on the caller's +/// stack (`corpus ingest`, octad export), so a statement deeper than this +/// is cut off and marked incomplete rather than allowed to overflow it. +/// The shipped corpora reach a bracket depth in the fifties. const MAX_NESTING: usize = 256; impl Parser { @@ -1182,6 +1219,9 @@ impl Parser { fn expr(&mut self, min_prec: u8) -> Node { let mut left = self.app(); + // Operators applied so far at this level: a left-associative chain + // deepens `left` by one node each time. + let mut chain = 0usize; while let Some(op) = self.op_at() { let Some(prec) = precedence(op) else { break; @@ -1189,13 +1229,26 @@ impl Parser { if prec < min_prec { break; } + // Every operator nests the tree one level deeper, whether the + // chain grows left (`a + a + …`) or recurses right (`a -> a -> …`). + // Past MAX_NESTING the rest is skipped and the key marked + // incomplete, so neither this parser nor the recursive passes over + // the tree (`render`, `has_hole`, drop) can overflow the stack. + if self.depth + chain >= MAX_NESTING { + self.too_deep = true; + self.i = self.toks.len(); + break; + } self.i += 1; let rhs_min = if op == "ARROW" || op == "IFF" { prec } else { prec + 1 }; + chain += 1; + self.depth += chain; let right = self.expr(rhs_min); + self.depth -= chain; left = Node::Op(op, vec![left, right]); } left @@ -1610,6 +1663,77 @@ mod tests { assert!(structural_key("(equal (len (rev x)) (len x)))").complete); } + /// `drop_ascriptions` as `dk-shape-v1` shipped it (c03386b), with the + /// slice guarded. The linear version must agree with it exactly. + fn drop_ascriptions_reference(toks: &[Tk]) -> Vec { + let mut out: Vec = Vec::new(); + let mut i = 0usize; + while i < toks.len() { + if is_open(&toks[i]) { + let j = matching(toks, i); + let inner = between(toks, i, j); + let ids: Vec<&String> = inner + .iter() + .filter_map(|t| match t { + Tk::Id(s) => Some(s), + _ => None, + }) + .collect(); + let syms: Vec<&String> = inner + .iter() + .filter_map(|t| match t { + Tk::Sym(s) => Some(s), + _ => None, + }) + .collect(); + if ids.len() == 2 && syms.len() == 1 && syms[0] == "::" && sort_of(ids[1]).is_some() + { + out.push(Tk::Id(ids[0].clone())); + i = j + 1; + continue; + } + } + out.push(toks[i].clone()); + i += 1; + } + out + } + + #[test] + fn drop_ascriptions_matches_dk_shape_v1() { + for s in [ + "(x :: nat) + 0 = x", + "(f 0 :: nat) = f 0", + "((x) :: nat) = x", + "[x :: int] = y", + "(x :: foo) = x", + "(x :: nat", + "(", + "(x y :: nat) = z", + "((a :: nat) :: nat)", + "(x :: nat] + (y :: int)", + ] { + let toks = lex(s); + assert_eq!( + drop_ascriptions(&toks), + drop_ascriptions_reference(&toks), + "{s}" + ); + } + } + + proptest::proptest! { + #[test] + fn drop_ascriptions_agrees_with_reference_on_random_tokens( + picks in proptest::collection::vec(0usize..9, 0..60) + ) { + const ALPHABET: [&str; 9] = ["(", ")", "[", "]", "x", "nat", "::", "0", "+"]; + let s: String = picks.iter().map(|&p| ALPHABET[p]).collect::>().join(" "); + let toks = lex(&s); + proptest::prop_assert_eq!(drop_ascriptions(&toks), drop_ascriptions_reference(&toks)); + } + } + /// A string literal is one opaque atom; a formula wrapper is unwrapped. #[test] fn string_literals_are_atoms_and_formula_quotes_are_unwrapped() { @@ -1742,6 +1866,21 @@ mod tests { assert_eq!(s.key, structural_key("x = y").key); } + /// Flat operator chains nest the tree too: a right-associative chain + /// recurses once per operator and a left-associative one builds a tree + /// that deep. Both overflowed a test thread's stack before the bound. + #[test] + fn operator_chains_are_bounded() { + for chain in ["a -> ", "a + ", "a /\\ ", "a = "] { + let long = format!("{}a", chain.repeat(200_000)); + let k = structural_key(&long); + assert!(!k.complete, "{chain}"); + assert_eq!(k.key.len(), 64); + } + let short = format!("{}a", "a + ".repeat(100)); + assert!(structural_key(&short).complete); + } + /// The guard is a no-op on balanced input: keys stay as they were. #[test] fn balanced_input_keys_are_unchanged_by_the_bracket_guard() { diff --git a/src/rust/lexicon/scan.rs b/src/rust/lexicon/scan.rs index 3f48ae03..5884cc57 100644 --- a/src/rust/lexicon/scan.rs +++ b/src/rust/lexicon/scan.rs @@ -149,8 +149,10 @@ pub fn parse_pair(arg: &str) -> Result<(String, String)> { /// /// # Errors /// -/// The key is empty, contains characters outside `[a-z0-9_]`, or contains -/// `__`, which is reserved as the separator in pair file names. +/// The key is empty, contains characters outside `[a-z0-9_]`, contains +/// `__`, or starts or ends with `_`. `__` separates the two keys in a pair +/// file name, and a key at either edge of it must not supply a third `_` +/// (`a_:b` and `a:_b` would both write `pairs/a___b.jsonl`). pub fn validate_corpus_key(key: &str) -> Result<()> { if key.is_empty() || !key @@ -159,10 +161,14 @@ pub fn validate_corpus_key(key: &str) -> Result<()> { { bail!("corpus key `{key}` must be non-empty [a-z0-9_]"); } - // `pairs/__.jsonl` is unambiguous only if no key contains `__`. + // `pairs/__.jsonl` is unambiguous only if no key contains `__` + // and no key starts or ends with `_`. if key.contains("__") { bail!("corpus key `{key}` must not contain `__`"); } + if key.starts_with('_') || key.ends_with('_') { + bail!("corpus key `{key}` must not start or end with `_`"); + } Ok(()) } @@ -993,18 +999,39 @@ pub fn scan_pair( summary.generic_names_skipped += 1; continue; } + // The cap bounds each join per name: exact pairs per raw name, and + // folded pairs across the whole folded group, so many distinct raw + // names that fold together (`list.map`, `option.map`, …) cannot + // each slip under it. + let rows = |c: &Corpus, n: &String| c.by_name[n].len(); + let exact_product: usize = names_a + .iter() + .filter(|n| names_b.contains(*n)) + .map(|n| rows(a, n) * rows(b, n)) + .sum(); + let all_product = names_a.iter().map(|n| rows(a, n)).sum::() + * names_b.iter().map(|n| rows(b, n)).sum::(); + let folded_product = all_product - exact_product; + let folded_capped = folded_product > opts.max_pairs_per_name; + if folded_capped { + summary.name_pairs_capped += 1; + summary.statement_pairs_capped += folded_product; + } for na in names_a { for nb in names_b { let (ga, gb) = (&a.by_name[na], &b.by_name[nb]); - let product = ga.len() * gb.len(); - if product > opts.max_pairs_per_name { - summary.name_pairs_capped += 1; - summary.statement_pairs_capped += product; - continue; - } let join = if na == nb { + let product = ga.len() * gb.len(); + if product > opts.max_pairs_per_name { + summary.name_pairs_capped += 1; + summary.statement_pairs_capped += product; + continue; + } Join::NameExact } else { + if folded_capped { + continue; + } Join::NameFolded }; for &ia in ga { @@ -1290,6 +1317,53 @@ mod tests { assert!(preset_pairs("everything").is_none()); } + #[test] + fn the_name_cap_bounds_a_whole_folded_group() { + // Five raw names per side fold to `add_comm`; each raw pair is one + // statement pair, but together they make 25 folded pairs. + let side = |prefix: &str| { + Corpus::from_rows( + prefix, + (0..5) + .map(|i| { + ( + format!("{prefix}{i}.add_comm"), + format!("x + y = y + x + {i}"), + ) + }) + .chain(std::iter::once(( + "nat.add_comm".to_string(), + "x + y = y + x".to_string(), + ))), + ) + }; + let (a, b) = (side("a"), side("b")); + let opts = ScanOptions { + max_pairs_per_name: 4, + ..ScanOptions::default() + }; + let mut emitted = 0usize; + let s = scan_pair(&a, &b, &opts, &mut |_| { + emitted += 1; + Ok(()) + }) + .unwrap(); + assert_eq!( + s.candidates.name_folded.total(), + 0, + "folded group is capped" + ); + assert_eq!( + s.candidates.name_exact.total(), + 1, + "the exact name still joins" + ); + assert_eq!(s.name_pairs_capped, 1); + // 6 × 6 rows in the folded group, minus the one exact pair + assert_eq!(s.statement_pairs_capped, 35); + assert!(emitted >= 1); + } + #[test] fn pair_arguments_are_validated() { assert_eq!( @@ -1301,6 +1375,9 @@ mod tests { assert!(parse_pair("../etc:hol4").is_err()); // `a__b:c` and `a:b__c` would both write pairs/a__b__c.jsonl assert!(parse_pair("a__b:c").is_err()); + // `a_:b` and `a:_b` would both write pairs/a___b.jsonl + assert!(parse_pair("a_:b").is_err()); + assert!(parse_pair("a:_b").is_err()); } #[test] diff --git a/src/rust/main.rs b/src/rust/main.rs index fd3100c7..544a9e00 100644 --- a/src/rust/main.rs +++ b/src/rust/main.rs @@ -388,7 +388,8 @@ enum LexiconOp { /// Also emit pairs whose shared name is generic (`lemma3`, `aux`, `ex1`). #[arg(long)] keep_generic: bool, - /// Skip a shared name whose statement cross product exceeds this. + /// Skip a shared name whose statement cross product exceeds this: + /// exact pairs per raw name, folded pairs per whole folded group. #[arg(long, default_value_t = 64)] max_pairs_per_name: usize, /// Skip a shape or skeleton group larger than this on either side. From de61f4b61ad6b0c8a4fd835faaa2948a60b4e0fd Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 27 Oct 2026 05:58:16 +0000 Subject: [PATCH 14/16] fix(corpus): a binary-only prefix operator with one operand is incomplete `(= (+ x 1))` built `(EQ (ADD v0 1))` and was marked complete. Relations, `->`/iff, membership, div and mod given one operand in prefix form now mark the key incomplete; unary minus, `not` and ACL2's one-argument `(+ x)` stay complete. No key changes. ADR numbers refreshed from a full rescan. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01WS4mfQeC3N1DWjcCQJaQqw --- CHANGELOG.adoc | 3 +- docs/CORPUS.adoc | 3 +- ...9-lexicon-v2-and-identity-arbitration.adoc | 27 +++++++-------- src/rust/corpus/canonical.rs | 33 +++++++++++++++++-- 4 files changed, 48 insertions(+), 18 deletions(-) diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index 57e2779a..863edd14 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -43,7 +43,8 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning]. collisions; coverage moves by at most 0.1 point per corpus. * *`+StructuralKey::complete+`* (new, `+#[serde(default)]+`) reports whether the shape accounts for the whole statement: false when the - parser stops early, invents a missing operand, or the input ends inside + parser stops early, invents a missing operand, gives a binary-only + prefix operator one operand (`+(= (+ x 1))+`), or the input ends inside an open bracket, a quoted statement or a block comment; when a closer meets a group of another kind; when the statement meets notation `+dk-shape-v1+` has no rule for (HOL binders, `+~+`, `+==>+`, diff --git a/docs/CORPUS.adoc b/docs/CORPUS.adoc index 725f739a..3a2e3e42 100644 --- a/docs/CORPUS.adoc +++ b/docs/CORPUS.adoc @@ -244,7 +244,8 @@ consumer that only compares one field should compare both. A key is only as good as the parse behind it. `+StructuralKey::complete+` says whether the canonicaliser read the *whole* statement; when it did not -(its parser stopped early or invented an operand, the input ended inside an +(its parser stopped early, invented an operand or found a relation with one +operand, the input ended inside an open bracket, quote or comment, a closer met a group of another kind, it met notation it has no rule for — HOL's `+!+` and `+?+` binders, Isabelle's `+\<…>+` escapes — or a header drop discarded the statement's own leading diff --git a/docs/decisions/2026-10-19-lexicon-v2-and-identity-arbitration.adoc b/docs/decisions/2026-10-19-lexicon-v2-and-identity-arbitration.adoc index 62af8d3a..4ca5e125 100644 --- a/docs/decisions/2026-10-19-lexicon-v2-and-identity-arbitration.adoc +++ b/docs/decisions/2026-10-19-lexicon-v2-and-identity-arbitration.adoc @@ -334,7 +334,8 @@ statement it rarely falls back to its text tier; it returns a *structural-tier* key for the prefix it did read, and different statements share that prefix. `StructuralKey::complete` now says whether the whole statement was read. It is false when the parser stops early, invents a -missing operand (`x + 1 =`) or reaches the end inside an open bracket or +missing operand (`x + 1 =`), finds a binary-only prefix operator with one +operand (`(= (+ x 1))`), or reaches the end inside an open bracket or an unclosed `(assert …` wrapper (ACL2s goals truncated mid-expression), when a closer meets a group of another kind (`(x]`) or a quoted statement or block comment never closes, @@ -351,19 +352,19 @@ Share of each corpus read completely (`dk-shape-v1`, 2026-10-27): [cols="2,2,2,2,2",options="header"] |=== | Corpus | Distinct rows | Read completely | Keys shared by distinct statements | Homonymous names -| acl2 | 135963 | 16.0 % | 783 | 8.0 % +| acl2 | 135963 | 15.9 % | 779 | 8.0 % | acl2s | 112742 | 4.8 % | 330 | 4.8 % -| afp | 102717 | 10.7 % | 530 | 2.1 % -| agda | 46028 | 40.9 % | 579 | 8.6 % +| afp | 102717 | 10.6 % | 525 | 2.1 % +| agda | 46028 | 40.8 % | 577 | 8.6 % | dafny | 10487 | 53.8 % | 153 | 12.2 % | dedukti | 1453 | 75.4 % | 54 | 20.6 % -| hol4 | 95738 | 8.7 % | 106 | 4.2 % +| hol4 | 95738 | 8.7 % | 104 | 4.2 % | hol_light | 43937 | 1.9 % | 15 | 2.9 % | isabelle_zf | 3577 | 0.4 % | 0 | 0.3 % -| lambda_prolog | 24897 | 93.5 % | 119 | 50.0 % -| lean3 | 92695 | 26.0 % | 2677 | 19.2 % -| mizar | 76522 | 19.4 % | 444 | 1.8 % -| why3 | 25180 | 28.3 % | 358 | 21.9 % +| lambda_prolog | 24897 | 93.5 % | 118 | 50.0 % +| lean3 | 92695 | 25.8 % | 2655 | 19.2 % +| mizar | 76522 | 19.2 % | 434 | 1.8 % +| why3 | 25180 | 27.2 % | 346 | 21.9 % |=== "Keys shared by distinct statements" counts complete keys only. Most are @@ -408,12 +409,12 @@ identity keys (E6 `cross_prover_identity_key`) inherit all four causes. Over all 33 pairs: 167,040 same-name statement pairs, of which 1,070 are exact cognates, 2,631 shape cognates, 64 skeleton (specialisation) -candidates, 5,777 differ, and 157,498 (94 %) are `unparsed`. A further +candidates, 5,458 differ, and 157,817 (94 %) are `unparsed`. A further 90,191 statement pairs under 308 over-large names are counted, not emitted: the per-name cap (64) bounds exact pairs per raw name and folded pairs per folded name. Synonym candidates under different names: 315 by -identical text, 433 by shape, 819 by skeleton. Debug build: 167 s for all thirteen corpora, almost all -of it loading and canonicalising; one pair scans in about a second. +identical text, 433 by shape, 819 by skeleton. Debug build: 169 s for all +thirteen corpora, almost all of it loading and canonicalising; one pair scans in about a second. * *HOL4 ↔ HOL Light* (pilot pair): 1,033 exact cognates and 144 text synonyms (`FACT_0` / `pth_0`), but 5,555 same-name pairs `unparsed`: @@ -433,7 +434,7 @@ of it loading and canonicalising; one pair scans in about a second. short-name rule above), fewer than three constants, or a bare type signature (λProlog's `int -> int -> int` against Dedukti's `Int -> Int -> Int`) say nothing about which statement it is. Joins - between different names skip them (3,279 groups, counted). + between different names skip them (3,253 groups, counted). === Equivalence by invariant and by witness diff --git a/src/rust/corpus/canonical.rs b/src/rust/corpus/canonical.rs index da26756d..2417b4b2 100644 --- a/src/rust/corpus/canonical.rs +++ b/src/rust/corpus/canonical.rs @@ -130,7 +130,8 @@ pub struct StructuralKey { pub tier: KeyTier, /// Whether the shape accounts for the whole statement. False when the /// parser stopped early (anything but a trailing `.`/`,`/`;` or an - /// unmatched closing bracket left over) or invented a missing operand, + /// unmatched closing bracket left over), invented a missing operand, or + /// gave a binary-only prefix operator one operand (`(= (+ x 1))`), /// when the input ended inside an open bracket, quote or block comment /// (a statement truncated mid-group), when a closer met a group of /// another kind, when the body holds notation this scheme has no rule @@ -181,6 +182,15 @@ fn op_of(name: &str) -> Option<&'static str> { Some(op) } +/// Operators that always take two operands. Unary minus, `not`, and the +/// one-argument `(+ x)` / `(and x)` that ACL2 accepts are not listed. +fn is_binary_only(op: &str) -> bool { + matches!( + op, + "EQ" | "NEQ" | "LT" | "LE" | "GT" | "GE" | "IN" | "ARROW" | "IFF" | "DIV" | "MOD" + ) +} + /// Infix precedence. `ARROW`/`IFF` are right-associative, the rest are /// left-associative (see [`Parser::expr`]). fn precedence(op: &str) -> Option { @@ -1032,6 +1042,8 @@ struct Parser { /// The tree reached [`MAX_NESTING`]: a group was skipped as a hole, or /// the rest of an operator chain was skipped. too_deep: bool, + /// A prefix operator that needs two operands was given one. + under_arity: bool, } /// Deepest tree the parser builds. Each bracket group and each infix @@ -1054,6 +1066,7 @@ impl Parser { unclosed: 0, depth: 0, too_deep: false, + under_arity: false, } } @@ -1191,6 +1204,11 @@ impl Parser { if args.is_empty() { return Node::Name(op_name.to_string()); } + // A relation or other binary-only operator with one operand + // (`(= (+ x 1))`) is a truncated statement, not a shape. + if args.len() < 2 && is_binary_only(op_name) { + self.under_arity = true; + } return Node::Op(op_name, args); } let mut args: Vec = vec![head.clone()]; @@ -1391,8 +1409,8 @@ fn has_unread_notation(body: &[Tk]) -> bool { /// the header drop discarded only a declared head, no leading group was misread /// as a telescope, the body holds no unread notation, and the parser /// left only ignorable terminators or closing brackets, with no group -/// left open at end of input or skipped beyond [`MAX_NESTING`], and invented -/// no missing operand. +/// left open at end of input or skipped beyond [`MAX_NESTING`], invented +/// no missing operand, and gave no binary-only prefix operator one operand. fn normalise(statement: &str) -> (String, String, bool) { let (raw, terminated) = lex_flagged(statement); // Read over the whole statement, header included: a mismatched or @@ -1413,6 +1431,7 @@ fn normalise(statement: &str) -> (String, String, bool) { && parser.rest_is_ignorable() && parser.unclosed == 0 && !parser.too_deep + && !parser.under_arity && !unread && !dropped_body && !bound.misread; @@ -1661,6 +1680,10 @@ mod tests { assert!(structural_key("Lemma add_comm : forall x y : nat, x + y = y + x.").complete); // ACL2 extraction keeps the `defthm` form's closer at the end assert!(structural_key("(equal (len (rev x)) (len x)))").complete); + // one-operand prefix forms that are legitimate + for s in ["(= (- x) (- 0 x))", "(not (= x y))", "(= (+ x) x)"] { + assert!(structural_key(s).complete, "{s}"); + } } /// `drop_ascriptions` as `dk-shape-v1` shipped it (c03386b), with the @@ -1783,6 +1806,10 @@ mod tests { // change) and reported "(assert x y", "(assert (forall ((x Nat)) (= x x", + // a binary-only prefix operator given one operand + "(= (+ x 1))", + "(< x)", + "(implies (p x) (<= x))", // a closer of the wrong kind, or a stray one "(x + y] = z", "x + y) = z", From dbbc93afe74424872ba71fd86d37c242676367f0 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 27 Oct 2026 06:18:55 +0000 Subject: [PATCH 15/16] fix(corpus,lexicon): leading literals, anonymous names, type-only signatures, --format json - A quote opens a formula only when its close also ends the statement (or meets another quote or an Isabelle keyword), so `"a" == "z"` and `"b" == "z"` keep their literals and different keys. - Names that fold to the empty string (`_`) are indexed; `is_generic` and `--keep-generic` decide whether they join. - A shape with arrows, no variables and no operator but ARROW is a bare signature whatever its type names (`Tree -> Tree -> Tree`), so it no longer proposes a synonym. - `echidna --format json lexicon scan` prints one JCS summary object on stdout; timings stay on stderr. - ADR numbers refreshed from a full rescan. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01WS4mfQeC3N1DWjcCQJaQqw --- CHANGELOG.adoc | 8 ++- ...9-lexicon-v2-and-identity-arbitration.adoc | 6 +- src/rust/corpus/canonical.rs | 66 ++++++++++++++----- src/rust/lexicon/scan.rs | 50 ++++++++++++-- src/rust/main.rs | 17 ++++- src/rust/output.rs | 5 ++ tests/lexicon_scan_test.rs | 22 +++++++ 7 files changed, 148 insertions(+), 26 deletions(-) diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index 863edd14..220374ac 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -25,6 +25,10 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning]. The per-name cap (`+--max-pairs-per-name+`) bounds folded-name pairs across a whole folded group, not per raw-name pair. Corpus keys may not start or end with `+_+`, so pair file names stay unambiguous. + Anonymous names (`+_+`) are indexed like any other, so + `+--keep-generic+` now joins them. A bare signature over any type names + (`+Tree -> Tree -> Tree+`) no longer proposes a synonym. With the global + `+--format json+`, the scan prints one JCS summary object on stdout. ==== Fixed — canonicaliser, 2026-10-27 @@ -37,7 +41,9 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning]. after an Isabelle statement keyword. Elsewhere (`+s = "a//b"+`, ACL2 `+"Goal"+` hints, Why3 `+meta "…"+`) it is one constant, so its contents are no longer read as comments, operators or variables, and a backslash - escapes the next character. *Key change*: statements with such a literal + escapes the next character. A quote opens a formula only when its close + also ends the statement (or meets another quote or an Isabelle keyword), + so `+"a" == "z"+` keeps its leading literal. *Key change*: statements with such a literal get new keys; distinct literals no longer share one. On `+training_data/+` this splits a dozen Mizar and seven Why3 key collisions; coverage moves by at most 0.1 point per corpus. diff --git a/docs/decisions/2026-10-19-lexicon-v2-and-identity-arbitration.adoc b/docs/decisions/2026-10-19-lexicon-v2-and-identity-arbitration.adoc index 4ca5e125..53c6b964 100644 --- a/docs/decisions/2026-10-19-lexicon-v2-and-identity-arbitration.adoc +++ b/docs/decisions/2026-10-19-lexicon-v2-and-identity-arbitration.adoc @@ -355,7 +355,7 @@ Share of each corpus read completely (`dk-shape-v1`, 2026-10-27): | acl2 | 135963 | 15.9 % | 779 | 8.0 % | acl2s | 112742 | 4.8 % | 330 | 4.8 % | afp | 102717 | 10.6 % | 525 | 2.1 % -| agda | 46028 | 40.8 % | 577 | 8.6 % +| agda | 46028 | 40.8 % | 574 | 8.6 % | dafny | 10487 | 53.8 % | 153 | 12.2 % | dedukti | 1453 | 75.4 % | 54 | 20.6 % | hol4 | 95738 | 8.7 % | 104 | 4.2 % @@ -409,11 +409,11 @@ identity keys (E6 `cross_prover_identity_key`) inherit all four causes. Over all 33 pairs: 167,040 same-name statement pairs, of which 1,070 are exact cognates, 2,631 shape cognates, 64 skeleton (specialisation) -candidates, 5,458 differ, and 157,817 (94 %) are `unparsed`. A further +candidates, 5,469 differ, and 157,806 (94 %) are `unparsed`. A further 90,191 statement pairs under 308 over-large names are counted, not emitted: the per-name cap (64) bounds exact pairs per raw name and folded pairs per folded name. Synonym candidates under different names: 315 by -identical text, 433 by shape, 819 by skeleton. Debug build: 169 s for all +identical text, 433 by shape, 819 by skeleton. Debug build: 175 s for all thirteen corpora, almost all of it loading and canonicalising; one pair scans in about a second. * *HOL4 ↔ HOL Light* (pilot pair): 1,033 exact cognates and 144 text diff --git a/src/rust/corpus/canonical.rs b/src/rust/corpus/canonical.rs index 2417b4b2..4e472158 100644 --- a/src/rust/corpus/canonical.rs +++ b/src/rust/corpus/canonical.rs @@ -369,7 +369,7 @@ fn lex_flagged(src: &str) -> (Vec, bool) { if j >= n { terminated = false; } - if opens_formula(out.last()) { + if opens_formula(out.last()) && closes_formula(&chars[(j + 1).min(n)..]) { let (inner_toks, inner_ok) = lex_flagged(&inner); terminated &= inner_ok; out.extend(inner_toks); @@ -432,25 +432,50 @@ fn lex_flagged(src: &str) -> (Vec, bool) { (out, terminated) } -/// Whether a quote after `prev` wraps a formula rather than a string +/// Isabelle words that open or continue a quoted statement. +const FORMULA_KEYWORDS: [&str; 9] = [ + "lemma", + "theorem", + "corollary", + "proposition", + "schematic_goal", + "assumes", + "shows", + "obtains", + "and", +]; + +/// Whether a quote after `prev` can wrap a formula rather than a string /// literal: at the start of the statement, after a `:` (`lemma foo: "…"`), -/// or after an Isabelle statement keyword. +/// or after an Isabelle statement keyword. [`closes_formula`] must also +/// hold for the text after the closing quote. fn opens_formula(prev: Option<&Tk>) -> bool { - const KEYWORDS: [&str; 9] = [ - "lemma", - "theorem", - "corollary", - "proposition", - "schematic_goal", - "assumes", - "shows", - "obtains", - "and", - ]; match prev { None => true, Some(Tk::Sym(s)) => s == ":", - Some(Tk::Id(s)) => KEYWORDS.contains(&s.as_str()), + Some(Tk::Id(s)) => FORMULA_KEYWORDS.contains(&s.as_str()), + _ => false, + } +} + +/// Whether the text after a closing quote ends the quoted statement: the +/// end of input or a terminator, another quoted proposition +/// (`assumes "A" "B"`), or an Isabelle keyword (`shows`, `and`, `for`, …). +/// Anything else (`"a" == "z"`) means the quote was a string literal. +fn closes_formula(rest: &[char]) -> bool { + const FOLLOWERS: [&str; 6] = ["for", "if", "where", "using", "unfolding", "by"]; + let rest: Vec = rest + .iter() + .copied() + .skip_while(|c| c.is_whitespace()) + .collect(); + match rest.first() { + None | Some('"') => true, + Some('.' | ';') => rest[1..].iter().all(|c| c.is_whitespace()), + Some(c) if is_ident_start(*c) => { + let word: String = rest.iter().take_while(|c| is_ident_char(**c)).collect(); + FORMULA_KEYWORDS.contains(&word.as_str()) || FOLLOWERS.contains(&word.as_str()) + }, _ => false, } } @@ -1774,6 +1799,17 @@ mod tests { structural_key("s = \"a \\\" c\"").key, "an escaped quote does not end the literal" ); + // a literal at the start of the statement is still a literal when + // the statement goes on after it + assert_ne!( + structural_key("\"a\" == \"z\"").key, + structural_key("\"b\" == \"z\"").key + ); + // Isabelle's quoted assumptions and conclusion are all unwrapped + assert_eq!( + structural_key("assumes \"x = y\" shows \"y = x\"").shape, + structural_key("assumes x = y shows y = x").shape + ); let bare = structural_key("x + y = y + x").key; for s in ["\"x + y = y + x\"", "lemma add_comm: \"x + y = y + x\""] { assert_eq!(structural_key(s).key, bare, "{s}"); diff --git a/src/rust/lexicon/scan.rs b/src/rust/lexicon/scan.rs index 5884cc57..4342ee0b 100644 --- a/src/rust/lexicon/scan.rs +++ b/src/rust/lexicon/scan.rs @@ -357,10 +357,11 @@ impl Corpus { for (i, e) in entries.iter().enumerate() { by_name.entry(e.name.clone()).or_default().push(i); by_statement.entry(e.statement.clone()).or_default().push(i); + // An anonymous name (`_`) folds to the empty string. It is indexed + // like any other: `is_generic` and `--keep-generic` decide whether + // it joins, and the other joins already treat it as a shared name. let folded = fold_name(&e.name); - if !folded.is_empty() { - by_fold.entry(folded).or_default().insert(e.name.clone()); - } + by_fold.entry(folded).or_default().insert(e.name.clone()); // Only a complete parse can stand for its statement in a join; // an incomplete shape is a prefix that other statements share. let k = &keys[e.key]; @@ -800,6 +801,13 @@ const TYPE_ATOMS: [&str; 9] = [ "ARROW", "NAT", "INT", "BOOL", "REAL", "TYPE", "STRING", "LIST", "VEC", ]; +/// `dk-shape-v1`'s canonical operators other than `ARROW`: the marks of a +/// statement rather than a type. +const NON_TYPE_OPERATORS: [&str; 17] = [ + "ADD", "MUL", "SUB", "DIV", "MOD", "EQ", "NEQ", "LT", "LE", "GT", "GE", "AND", "OR", "NOT", + "IFF", "IN", "APPEND", +]; + /// Whether a skeleton carries enough structure to propose a synonym between /// two *differently named* statements: at least three non-variable atoms, /// at least one of them outside the type language, and no variable applied @@ -808,7 +816,10 @@ const TYPE_ATOMS: [&str; 9] = [ /// `(EQ (v0 0) 1)`; a variable in function position is the mark of that. /// A bare `(summable v0)` says only that something is summable, and a bare /// signature such as `int -> int -> int` is shared by every function of -/// that type. Name joins are not filtered: there the shared name anchors. +/// that type. So is `Tree -> Tree -> Tree`, whose type is not a canonical +/// sort: a shape with arrows, no variables and no operator besides `ARROW` +/// is a signature whatever its type names. Name joins are not filtered: +/// there the shared name anchors. pub fn informative(skeleton: &str) -> bool { let chars: Vec = skeleton.chars().collect(); let variable_head = chars.windows(3).enumerate().any(|(i, w)| { @@ -827,7 +838,13 @@ pub fn informative(skeleton: &str) -> bool { }) .collect(); let beyond_types = constants.iter().any(|t| !TYPE_ATOMS.contains(t)); - !variable_head && constants.len() >= 3 && beyond_types + let has_variable = skeleton + .split(|c: char| c.is_whitespace() || matches!(c, '(' | ')' | '[' | ']')) + .any(|t| t.len() > 1 && t.starts_with('v') && t[1..].chars().all(|c| c.is_ascii_digit())); + let bare_signature = !has_variable + && constants.contains(&"ARROW") + && !constants.iter().any(|t| NON_TYPE_OPERATORS.contains(t)); + !variable_head && constants.len() >= 3 && beyond_types && !bare_signature } /// Jaccard similarity of the shapes' non-variable atoms in thousandths, @@ -1317,6 +1334,25 @@ mod tests { assert!(preset_pairs("everything").is_none()); } + #[test] + fn anonymous_names_join_only_when_generic_names_are_kept() { + let side = + |key: &str| Corpus::from_rows(key, [("_".to_string(), "x + y = y + x".to_string())]); + let (a, b) = (side("a"), side("b")); + let run = |keep_generic: bool| { + let opts = ScanOptions { + keep_generic, + ..ScanOptions::default() + }; + scan_pair(&a, &b, &opts, &mut |_| Ok(())).unwrap() + }; + let skipped = run(false); + assert_eq!(skipped.generic_names_skipped, 1); + assert_eq!(skipped.candidates.name_exact.total(), 0); + let kept = run(true); + assert_eq!(kept.candidates.name_exact.total(), 1); + } + #[test] fn the_name_cap_bounds_a_whole_folded_group() { // Five raw names per side fold to `add_comm`; each raw pair is one @@ -1412,6 +1448,10 @@ mod tests { // ...and their skeletons, where sorts render as `?` assert!(!informative("(ARROW ? (ARROW ? ?))")); assert!(!informative("(ARROW ? ?)")); + // a signature over type names that are not canonical sorts + assert!(!informative("(ARROW Tree (ARROW Tree Tree))")); + // an implication between predicates of a variable is a statement + assert!(informative("(ARROW (prime v0) (odd v0))")); assert!(informative("(ARROW (LE v0 v1) (LE (ADD v0 1) (ADD v1 1)))")); } diff --git a/src/rust/main.rs b/src/rust/main.rs index 544a9e00..af3e42e0 100644 --- a/src/rust/main.rs +++ b/src/rust/main.rs @@ -583,7 +583,7 @@ async fn main() -> Result<()> { }, Commands::Lexicon { op } => { - lexicon_command(op)?; + lexicon_command(op, &formatter)?; }, Commands::Design { op } => { @@ -1383,7 +1383,7 @@ async fn diagnostics_command() -> Result<()> { /// old output file that cannot be removed, or a serialisation or output /// write failure. Also returns an error if the scan thread cannot be /// spawned or panics. Failed scans may leave partial output. -fn lexicon_command(op: LexiconOp) -> Result<()> { +fn lexicon_command(op: LexiconOp, formatter: &OutputFormatter) -> Result<()> { use echidna::lexicon::scan::{self, RunOptions, ScanOptions}; let LexiconOp::Scan { @@ -1435,6 +1435,19 @@ fn lexicon_command(op: LexiconOp) -> Result<()> { .map_err(|_| anyhow::anyhow!("the scan thread panicked"))??; let (report, out) = report; + if formatter.is_json() { + // One JCS object on stdout; the timings stay on stderr. + let summary = serde_json::json!({ + "coverage": report.coverage, + "pairs": report.pairs, + "out": out.display().to_string(), + "total_ms": u64::try_from(report.total.as_millis()).unwrap_or(u64::MAX), + }); + std::io::Write::write_all(&mut std::io::stdout(), &scan::jcs_line(&summary)?)?; + eprintln!("total: {:.2?}; output in {}", report.total, out.display()); + return Ok(()); + } + println!( "{:<14} {:>8} {:>8} {:>6} {:>7} {:>6} {:>6} {:>6} {:>8}", "corpus", "rows", "names", "hom%", "struct%", "skel%", "text%", "cmpl%", "collide" diff --git a/src/rust/output.rs b/src/rust/output.rs index b897b387..5f70548b 100644 --- a/src/rust/output.rs +++ b/src/rust/output.rs @@ -53,6 +53,11 @@ impl OutputFormatter { Self { format } } + /// Whether output is machine-readable JSON (`--format json`). + pub fn is_json(&self) -> bool { + matches!(self.format, OutputFormat::Json) + } + /// Output a success message pub fn success(&self, message: &str) -> Result<()> { match self.format { diff --git a/tests/lexicon_scan_test.rs b/tests/lexicon_scan_test.rs index 4b3033e0..764ec669 100644 --- a/tests/lexicon_scan_test.rs +++ b/tests/lexicon_scan_test.rs @@ -233,3 +233,25 @@ fn a_rerun_with_fewer_pairs_leaves_no_stale_pair_files() { ); let _ = std::fs::remove_dir_all(&out); } + +#[test] +fn the_global_json_format_prints_one_parseable_object() { + let out = tempfile::tempdir().expect("tempdir"); + let run = std::process::Command::new(env!("CARGO_BIN_EXE_echidna")) + .args(["--format", "json", "lexicon", "scan", "--training-dir"]) + .arg(fixtures()) + .args(["--pair", "hol4_mini:hol_light_mini", "--out"]) + .arg(out.path()) + .output() + .expect("run echidna lexicon scan"); + assert!( + run.status.success(), + "{}", + String::from_utf8_lossy(&run.stderr) + ); + let stdout = String::from_utf8(run.stdout).expect("utf-8"); + assert_eq!(stdout.lines().count(), 1, "one JSON line: {stdout}"); + let v: serde_json::Value = serde_json::from_str(&stdout).expect("stdout is JSON"); + assert_eq!(v["pairs"][0]["pair"][0], "hol4_mini"); + assert_eq!(v["coverage"].as_array().map(Vec::len), Some(2)); +} From 428a726dc645cd92997bd9431c828f7d740cdb2a Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 27 Oct 2026 06:46:04 +0000 Subject: [PATCH 16/16] fix(corpus,lexicon): adjacent Isabelle propositions, hyphenated corpus keys, honest identity message - A quote right after an unwrapped formula is the next proposition (`assumes "P x" "Q x"`), not a string literal. - Corpus keys may contain `-`, so the shipped `2026-03-20` corpus scans. - `corpus identity` says "no completely read declarations" when every match was skipped as incomplete, instead of "no declarations". A full rescan of the 13 corpora gives the same numbers as before. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01WS4mfQeC3N1DWjcCQJaQqw --- CHANGELOG.adoc | 4 +++- src/rust/corpus/canonical.rs | 12 +++++++++++- src/rust/lexicon/scan.rs | 11 +++++++---- src/rust/main.rs | 9 ++++++++- 4 files changed, 29 insertions(+), 7 deletions(-) diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index 220374ac..22a3e899 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -24,7 +24,8 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning]. removes only the file names the scan writes. The per-name cap (`+--max-pairs-per-name+`) bounds folded-name pairs across a whole folded group, not per raw-name pair. Corpus keys may not - start or end with `+_+`, so pair file names stay unambiguous. + start or end with `+_+`, so pair file names stay unambiguous; a hyphen is + allowed, so the shipped `+2026-03-20+` corpus can be scanned. Anonymous names (`+_+`) are indexed like any other, so `+--keep-generic+` now joins them. A bare signature over any type names (`+Tree -> Tree -> Tree+`) no longer proposes a synonym. With the global @@ -43,6 +44,7 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning]. are no longer read as comments, operators or variables, and a backslash escapes the next character. A quote opens a formula only when its close also ends the statement (or meets another quote or an Isabelle keyword), + and a quote right after an unwrapped formula is the next proposition, so `+"a" == "z"+` keeps its leading literal. *Key change*: statements with such a literal get new keys; distinct literals no longer share one. On `+training_data/+` this splits a dozen Mizar and seven Why3 key diff --git a/src/rust/corpus/canonical.rs b/src/rust/corpus/canonical.rs index 4e472158..996f751e 100644 --- a/src/rust/corpus/canonical.rs +++ b/src/rust/corpus/canonical.rs @@ -322,6 +322,9 @@ fn lex(src: &str) -> Vec { /// runs off the end of the input (part of the statement was swallowed). fn lex_flagged(src: &str) -> (Vec, bool) { let mut terminated = true; + // `out.len()` just after an unwrapped formula: a quote right there is + // the next proposition (`assumes "P x" "Q x"`), not a string literal. + let mut after_wrapper: Option = None; let chars: Vec = src.chars().collect(); let n = chars.len(); let mut out: Vec = Vec::new(); @@ -369,10 +372,12 @@ fn lex_flagged(src: &str) -> (Vec, bool) { if j >= n { terminated = false; } - if opens_formula(out.last()) && closes_formula(&chars[(j + 1).min(n)..]) { + let wrapper_position = opens_formula(out.last()) || after_wrapper == Some(out.len()); + if wrapper_position && closes_formula(&chars[(j + 1).min(n)..]) { let (inner_toks, inner_ok) = lex_flagged(&inner); terminated &= inner_ok; out.extend(inner_toks); + after_wrapper = Some(out.len()); } else { out.push(Tk::Name(format!("\"{inner}\""))); } @@ -1810,6 +1815,11 @@ mod tests { structural_key("assumes \"x = y\" shows \"y = x\"").shape, structural_key("assumes x = y shows y = x").shape ); + // adjacent quoted propositions are all formulas + assert_eq!( + structural_key("assumes \"x = y\" \"y = z\" shows \"x = z\"").shape, + structural_key("assumes x = y y = z shows x = z").shape + ); let bare = structural_key("x + y = y + x").key; for s in ["\"x + y = y + x\"", "lemma add_comm: \"x + y = y + x\""] { assert_eq!(structural_key(s).key, bare, "{s}"); diff --git a/src/rust/lexicon/scan.rs b/src/rust/lexicon/scan.rs index 4342ee0b..7d34a846 100644 --- a/src/rust/lexicon/scan.rs +++ b/src/rust/lexicon/scan.rs @@ -149,7 +149,8 @@ pub fn parse_pair(arg: &str) -> Result<(String, String)> { /// /// # Errors /// -/// The key is empty, contains characters outside `[a-z0-9_]`, contains +/// The key is empty, contains characters outside `[a-z0-9_-]` (the shipped +/// `proof_states_2026-03-20.jsonl` needs the hyphen), contains /// `__`, or starts or ends with `_`. `__` separates the two keys in a pair /// file name, and a key at either edge of it must not supply a third `_` /// (`a_:b` and `a:_b` would both write `pairs/a___b.jsonl`). @@ -157,9 +158,9 @@ pub fn validate_corpus_key(key: &str) -> Result<()> { if key.is_empty() || !key .chars() - .all(|c| c.is_ascii_lowercase() || c.is_ascii_digit() || c == '_') + .all(|c| c.is_ascii_lowercase() || c.is_ascii_digit() || c == '_' || c == '-') { - bail!("corpus key `{key}` must be non-empty [a-z0-9_]"); + bail!("corpus key `{key}` must be non-empty [a-z0-9_-]"); } // `pairs/__.jsonl` is unambiguous only if no key contains `__` // and no key starts or ends with `_`. @@ -1413,6 +1414,8 @@ mod tests { assert!(parse_pair("a__b:c").is_err()); // `a_:b` and `a:_b` would both write pairs/a___b.jsonl assert!(parse_pair("a_:b").is_err()); + // the shipped `proof_states_2026-03-20.jsonl` corpus + assert!(parse_pair("2026-03-20:lean3").is_ok()); assert!(parse_pair("a:_b").is_err()); } @@ -1481,7 +1484,7 @@ mod tests { assert!(!is_pair_file_name("hol4__Hol.jsonl")); assert!(!is_pair_file_name("hol4__hol_light.json")); assert!(is_collision_file_name("lean3.jsonl")); - assert!(!is_collision_file_name("my-export.jsonl")); + assert!(!is_collision_file_name("notes.v2.jsonl")); assert!(!is_collision_file_name("lean3.txt")); } diff --git a/src/rust/main.rs b/src/rust/main.rs index af3e42e0..a2b4ed4c 100644 --- a/src/rust/main.rs +++ b/src/rust/main.rs @@ -1861,7 +1861,14 @@ fn corpus_command(op: CorpusOp, formatter: &OutputFormatter) -> Result<()> { ))?; } if groups.is_empty() { - formatter.info(&format!("no declarations matching '{}'", pattern))?; + // When every match was skipped, the name is present but carries + // no identity; saying "no declarations" would mislead. + let what = if skipped_incomplete > 0 { + "no completely read declarations" + } else { + "no declarations" + }; + formatter.info(&format!("{what} matching '{}'", pattern))?; return Ok(()); }