From c9e45f82b778cb222eab611ac4384e0f3f1353ff Mon Sep 17 00:00:00 2001 From: Vasilev Dmitrii Date: Sat, 29 Aug 2026 08:40:50 +0700 Subject: [PATCH] feat(tri): `tri discard classify` -- what the parser stopped on, grouped A ranked list says WHERE the tokens are. It does not say whether the top six entries are six problems or one. They were one: class specs tokens forall/==> (quantified) 38 20991 var/const statement 18 7020 assert 17 1853 other 14 587 TOTAL 87 30451 Sixty-nine percent of what is left is a construct the grammar does not contain -- quantified invariants, `forall x : T ... ==> ...`, in 38 specs mostly under specs/igla/race/. That is a language decision, not a parser rung: what a universally quantified invariant means at codegen commits four backends, and `==>` lowered to `!a || b` makes a false antecedent a pass, which is the vacuous shape `no-vacuous-invariant` exists to catch arriving through the front door. Filed as #2774 rather than implemented. Two things worth pinning, and both are tested: * CLASSES is ordered and first match wins. A quantified invariant whose body also declares a `var` must land in the quantified bucket; reordering the list silently re-attributes thousands of tokens. * `==>` NEVER APPEARS IN A DROP TRACE. The lexer splits it, so the trace reads `== 4 == >`. A matcher for the source spelling finds zero of the 38, and the conclusion would have been that the construct is rare. A spec that yields no trace is counted separately and NOT as `other`: no trace was read, so no cause is claimed. Skill 159-161: rank to find the biggest, classify before deciding what KIND of work it is; match what the trace says rather than what the source says, because the lexer sits between them and is the thing under investigation; and a number written before it was measured is still a wrong number. Refs #2774 Co-Authored-By: Claude Opus 5 --- .claude/skills/ci-gates/SKILL.md | 43 +++++++ cli/tri/src/discard.rs | 114 +++++++++++++++++- ...percent-of-the-discard-is-one-construct.md | 8 ++ 3 files changed, 164 insertions(+), 1 deletion(-) create mode 100644 docs/now/2026-08-29-sixty-nine-percent-of-the-discard-is-one-construct.md diff --git a/.claude/skills/ci-gates/SKILL.md b/.claude/skills/ci-gates/SKILL.md index b2eb7a6e8c..cae167c369 100644 --- a/.claude/skills/ci-gates/SKILL.md +++ b/.claude/skills/ci-gates/SKILL.md @@ -5692,3 +5692,46 @@ run. **A stale limitation there is worse than a stale feature list** — it eith frightens people away from a check that works, or excuses them from one that does. Re-verify that section by running its claims, not by reading them. + +## 159. A ranked list says where; it does not say whether the top six are one problem + +`tri discard top` put six `specs/igla/race/*` files at the head of the list. Six +entries, ~7 000 tokens. It looked like six rungs. + +Classifying the drop traces said otherwise: + + forall/==> (quantified) 38 specs 20991 tokens + var/const statement 18 7020 + assert 17 1853 + other 14 587 + +**Sixty-nine percent of what remained was one construct the grammar does not +contain** — quantified invariants. Not a parser rung at all: a language decision +about what `forall x : T … ==> …` means at codegen, which commits four backends +and belongs to the owner (#2774). + +Rank to find the biggest. **Classify before deciding what kind of work it is.** + +## 160. The lexer had already split the token I was grepping for + +`==>` never appears in a drop trace. The lexer emits `==` and `>`, so the trace +reads + + dropped: input . activations . len == 4 == > + +A matcher looking for `==>` would have found zero of the thirty-eight specs and I +would have concluded the construct was rare. Match what the trace actually says, +not what the source says — there is a lexer between them, and it is the thing +under investigation. + +## 161. A number written before it was measured is still a wrong number + +A commit message of mine said `cargo test 2430 passed`. The measurement is 2429: +I had assumed the new conformance case would add one, and it does not — +`parse-conform` is a `t27c` subcommand, not a cargo test. + +Nobody would have caught it. It sat in a paragraph of numbers that were all +measured, which is exactly what makes one unmeasured number dangerous. + +Corrected by a follow-up commit, not an amend (see 155). **Write the number after +running the command, in the same minute, or do not write it.** diff --git a/cli/tri/src/discard.rs b/cli/tri/src/discard.rs index ccbc85a080..5605920a95 100644 --- a/cli/tri/src/discard.rs +++ b/cli/tri/src/discard.rs @@ -29,8 +29,29 @@ pub enum DiscardCmd { #[arg(long, default_value_t = 15)] n: usize, }, + /// Group the discard by what the parser stopped on. + /// + /// A ranked list says where the tokens are; it does not say whether the top + /// six are six problems or one. They were one: 38 specs and 20 991 of the + /// 30 451 tokens are quantified invariants (`forall x : T ... ==>`), a + /// construct the grammar does not contain (#2774). That is a language + /// decision, not a parser rung, and the ranking alone could not tell. + Classify, } +/// The buckets, in the order they are TESTED -- first match wins, so the more +/// specific pattern must come first. `forall` before `var`, because a quantified +/// invariant's body often declares one too. +/// +/// This is a coarse keyword match over `parse-complete --show` traces, and it +/// says so: `other` is where anything mis-binned lands, and a large `other` is +/// the signal that these buckets have stopped describing the corpus. +const CLASSES: [(&str, &[&str]); 3] = [ + ("forall/==> (quantified)", &["forall", "==>", "== >"]), + ("var/const statement", &["dropped: var ", "dropped: const "]), + ("assert", &["assert"]), +]; + fn repo_root() -> Result { let out = std::process::Command::new("git") .args(["rev-parse", "--show-toplevel"]) @@ -110,12 +131,77 @@ fn pinned(root: &std::path::Path) -> Result>> { Ok(map) } +/// The drop trace for one spec, as `t27c parse-complete --show` prints it. +fn drop_trace(root: &std::path::Path, spec: &str) -> Option { + let t27c = ["target/release/t27c", "target/debug/t27c"] + .iter() + .map(|p| root.join(p)) + .find(|p| p.is_file())?; + let out = std::process::Command::new(t27c) + .args(["parse-complete", "--show", spec]) + .current_dir(root) + .output() + .ok()?; + Some(String::from_utf8_lossy(&out.stdout).to_string()) +} + +fn classify(root: &std::path::Path, obs: &BTreeMap) -> Result<()> { + let mut specs: BTreeMap<&str, usize> = BTreeMap::new(); + let mut toks: BTreeMap<&str, usize> = BTreeMap::new(); + let mut unread = 0usize; + for (spec, n) in obs { + let Some(trace) = drop_trace(root, spec) else { + // Not "other". No trace was read, so no cause is claimed. + unread += 1; + continue; + }; + let dropped: String = trace + .lines() + .filter(|l| l.trim_start().starts_with("dropped:")) + .collect::>() + .join("\n"); + let name = CLASSES + .iter() + .find(|(_, pats)| pats.iter().any(|p| dropped.contains(p))) + .map(|(n, _)| *n) + .unwrap_or("other"); + *specs.entry(name).or_default() += 1; + *toks.entry(name).or_default() += n; + } + let mut rows: Vec<_> = toks.iter().collect(); + rows.sort_by(|a, b| b.1.cmp(a.1)); + println!(" {:<26} {:>6} {:>9}", "class", "specs", "tokens"); + for (name, t) in rows { + println!(" {:<26} {:>6} {:>9}", name, specs[*name], t); + } + println!( + " {:<26} {:>6} {:>9}", + "TOTAL", + specs.values().sum::(), + toks.values().sum::() + ); + if unread > 0 { + println!(); + println!(" {unread} spec(s) yielded no trace -- NOT counted as `other`."); + } + println!(); + println!(" Coarse keyword match over `parse-complete --show`. A large `other`"); + println!(" means these buckets have stopped describing the corpus, not that"); + println!(" the corpus has stopped having causes."); + Ok(()) +} + pub fn run(cmd: &DiscardCmd) -> Result<()> { let root = repo_root()?; let obs = observed(&root)?; + if matches!(cmd, DiscardCmd::Classify) { + return classify(&root, &obs); + } let pin = pinned(&root)?; - let DiscardCmd::Top { n } = cmd; + let DiscardCmd::Top { n } = cmd else { + unreachable!("Classify returned above") + }; let mut rows: Vec<(&String, &usize)> = obs.iter().collect(); rows.sort_by(|a, b| b.1.cmp(a.1).then(a.0.cmp(b.0))); @@ -164,6 +250,32 @@ mod tests { assert_eq!(n, 208); } + /// First match wins, so a quantified invariant whose body also declares a + /// `var` must land in the quantified bucket. Reordering CLASSES silently + /// re-attributes thousands of tokens, which is why the order is tested. + #[test] + fn the_more_specific_class_is_tested_first() { + let trace = "dropped: forall x : T\ndropped: var y = 1 ;"; + let name = super::CLASSES + .iter() + .find(|(_, pats)| pats.iter().any(|p| trace.contains(p))) + .map(|(n, _)| *n) + .unwrap_or("other"); + assert_eq!(name, "forall/==> (quantified)"); + } + + /// `==>` reaches the trace as `== >` because the lexer splits it. A matcher + /// that only looked for `==>` would report zero of the 38 specs. + #[test] + fn the_split_implication_arrow_is_matched() { + let trace = "dropped: input . activations . len == 4 == >"; + let hit = super::CLASSES[0].1.iter().any(|p| trace.contains(p)); + assert!( + hit, + "the lexer splits `==>`; match what the trace actually says" + ); + } + /// A summary line must not be mistaken for a spec row. #[test] fn the_summary_lines_are_not_rows() { diff --git a/docs/now/2026-08-29-sixty-nine-percent-of-the-discard-is-one-construct.md b/docs/now/2026-08-29-sixty-nine-percent-of-the-discard-is-one-construct.md new file mode 100644 index 0000000000..6f557893d7 --- /dev/null +++ b/docs/now/2026-08-29-sixty-nine-percent-of-the-discard-is-one-construct.md @@ -0,0 +1,8 @@ +# NOW -- Sixty-nine percent of the discard is one construct (2026-08-29) + +## Sixty-nine percent of the discard is one construct (Refs #2774) + +- tri discard classify: forall/==> 38 specs 20991 tokens, var/const 18/7020, assert 17/1853, other 14/587 +- a ranked list said where the tokens are, not whether the top six were six problems or one -- they were one +- quantified invariants are a language decision, not a parser rung: what forall means at codegen commits four backends (#2774) +- ==> never appears in a drop trace; the lexer splits it into == and >, so a matcher for the source spelling would have found zero of 38