diff --git a/.claude/skills/ci-gates/SKILL.md b/.claude/skills/ci-gates/SKILL.md index cae167c369..c83c228770 100644 --- a/.claude/skills/ci-gates/SKILL.md +++ b/.claude/skills/ci-gates/SKILL.md @@ -5735,3 +5735,87 @@ 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.** + +## 162. Ask the parser what it dropped instead of grepping what it printed + +Yesterday's `tri discard classify` was a keyword match over printed traces: it saw +the word `forall` and called the bucket `forall`. The parser already writes down +every token it throws away, so the question could be asked of the record instead. + +Two answers changed: + + heuristic: forall/==> ......... 20 991 + record: bdd-block-fallback ... 23 852 (78%, one channel) + brace-body ........... 4 602 + top-level-resync ..... 1 894 + +And the head token is not the channel. `given` was the fourth-largest head at +2 453 tokens, which read like a fn-shaped defect worth thousands. Fixing that arm +recovered **43**. The other 2 410 came from braceless blocks falling back — a +different defect wearing the same first word. + +**A head token says what the parser stopped ON. A channel says which recovery +threw it away. Reporting one as the other overstates every fix you plan.** + +## 163. `zip` on two parallel vectors is a silent truncation + +I added a channel vector beside the existing span vector, pushed at "all three" +recording sites, and zipped them. The total came out 27 tokens short of +`parse-complete`'s — two more push sites existed at a different indentation and +my search pattern had missed them. + +`zip` truncated to the shorter side and reported a clean, plausible, wrong table. +Nothing failed. The only signal was a total that did not match another account of +the same thing. + + if spans.len() != channels.len() { return Err(...) } + +**Two vectors that must stay in lockstep need an assertion, not a `zip`.** And the +reason the gap was findable at all is that a second, independent account of the +same quantity already existed — which is the argument for keeping both. + +## 164. The parser named the shape, then threw it away + + // BDD-style fn: `fn name() given ... then ...` -- a keyword-style test + // spelled as a fn (linker.t27). Detect BEFORE return-type parsing. + if self.current.kind == TokenKind::Ident && self.current.lexeme == "given" { + self.skip_to_next_top_level(); // <- every clause, gone + return Ok(decl); + } + +The comment cites the exact file it silently empties. Someone understood the shape +well enough to special-case it and stopped one line short of lowering it. + +**A comment that names a construct beside a `skip` is a fix that was scoped and +not finished.** Grep for that pair: recognition followed by discard is a different +and better-signposted target than an unhandled shape nobody has looked at. + +## 165. Same file, two flag sets, opposite verdicts + +The elaboration ratchet said my change took `linker` from 4 errors to 6. I ran +iverilog on the same generated file and counted **fewer** errors than master. + +The gate runs `iverilog -g2012 -DSIMULATION`; I had run bare `iverilog`. Under +the default the file is Verilog-2005, where every size cast is an error and +master's *empty task* trips "Task body with no statements" — so master looked +worse. Under `-g2012` both of those are legal, the size casts vanish, and what +remains is the two errors my change actually added. + +**Copy the gate's invocation, flags included, out of its source.** A tool with +the right name and the wrong flags is a different tool, and it will happily +disagree with the gate about the same file. + +## 166. If a backend refuses to lower a construct, produce that construct + +A `fn` whose body is BDD clauses is a test spelled as a function. My first fix +kept it a `FnDecl` and filled the body, so `gen-verilog` — which emits RTL for +functions and deliberately does **not** lower tests — produced `\assert (…)` +inside a task and an assignment to the task's own name. + +The fix was not to teach the Verilog backend about a new fn flavour. It was to +emit a `TestBlock`, because that is what the source means. Every backend already +knows whether it lowers tests. + +**When recovered content lands in the wrong node kind, change the node, not the +four consumers.** The give-away is a fix that would need a matching change in +every backend: that is usually the parser choosing the wrong shape. diff --git a/.trinity/seals/Linker.json b/.trinity/seals/Linker.json index b0a1137813..2769352ba3 100644 --- a/.trinity/seals/Linker.json +++ b/.trinity/seals/Linker.json @@ -1,8 +1,8 @@ { - "gen_hash_c": "sha256:108d46508c8fe24bd3bca14b4b54d51c3d8827c6928c2f9be71995e446e0c857", - "gen_hash_rust": "sha256:f6ea2b804287146898f363f3c2f0f29e4185bc7a60ee3fc6c1a35e0a93143760", - "gen_hash_verilog": "sha256:78cfa653fb656438b2dff0eea3df9198dc1ade38253897016a7031868c63018d", - "gen_hash_zig": "sha256:e21e5e37dd9d05dea274649d7e956c7899d72bfe26285d9a78541993510c4d56", + "gen_hash_c": "sha256:af9eaaa325e9a0aa0f5fc783a9564b967a852322f1a63f947e02c13d65901948", + "gen_hash_rust": "sha256:e9e1f909a3f8773af1ccf6437cc65ae079945b7a57bde528760f7b5bca288037", + "gen_hash_verilog": "sha256:49b4eed7bfa531a9fa124bee2469bbab58cea99f818f0ee1609444d5a757006c", + "gen_hash_zig": "sha256:f928ec5f281b5df49d58d087284b04604e13c7dafa4c718d1bda8d7ed63a7f41", "module": "Linker", "ring": 12, "sealed_at": "2026-08-28T18:19:55Z", diff --git a/.trinity/seals/fpga_Linker.json b/.trinity/seals/fpga_Linker.json index 1633846256..edce6a5f99 100644 --- a/.trinity/seals/fpga_Linker.json +++ b/.trinity/seals/fpga_Linker.json @@ -1,12 +1,12 @@ { - "gen_hash_c": "sha256:108d46508c8fe24bd3bca14b4b54d51c3d8827c6928c2f9be71995e446e0c857", - "gen_hash_rust": "sha256:f6ea2b804287146898f363f3c2f0f29e4185bc7a60ee3fc6c1a35e0a93143760", - "gen_hash_verilog": "sha256:78cfa653fb656438b2dff0eea3df9198dc1ade38253897016a7031868c63018d", - "gen_hash_zig": "sha256:e21e5e37dd9d05dea274649d7e956c7899d72bfe26285d9a78541993510c4d56", + "gen_hash_c": "sha256:af9eaaa325e9a0aa0f5fc783a9564b967a852322f1a63f947e02c13d65901948", + "gen_hash_rust": "sha256:e9e1f909a3f8773af1ccf6437cc65ae079945b7a57bde528760f7b5bca288037", + "gen_hash_verilog": "sha256:49b4eed7bfa531a9fa124bee2469bbab58cea99f818f0ee1609444d5a757006c", + "gen_hash_zig": "sha256:f928ec5f281b5df49d58d087284b04604e13c7dafa4c718d1bda8d7ed63a7f41", "module": "Linker", "ring": 12, - "sealed_at": "2026-08-28T18:19:55Z", - "sealed_by": "t27c-bootstrap@0.1.0", + "sealed_at": "2026-08-29T02:47:18Z", + "sealed_by": "t27c-bootstrap@0.2.0", "spec_hash": "sha256:64a8091d1c5d8163af7ce400dee2b8ffbe713584045340e1126a0b7560b04c6e", "spec_path": "specs/fpga/linker.t27" -} +} \ No newline at end of file diff --git a/bootstrap/src/compiler.rs b/bootstrap/src/compiler.rs index b1c5871efa..92b0a6ee3f 100644 --- a/bootstrap/src/compiler.rs +++ b/bootstrap/src/compiler.rs @@ -1093,6 +1093,17 @@ pub struct Parser { /// told us 55,563 tokens vanish; only reading them can say whether any of /// it is content a theorem depends on. See T43. dropped_spans: Vec<(u32, String)>, + /// W699: WHICH recovery threw each token away, parallel to `dropped_spans`. + /// + /// The head token of a dropped run says what the parser stopped ON. It does + /// not say which of the four recovery channels did the dropping, and the two + /// are different questions: `given` is the fourth-largest head in the corpus + /// and only 43 of its 2 453 tokens came from the fn arm that names it. + dropped_channels: Vec<&'static str>, + /// Set by `restore_bdd_fallback` for the duration of its resync, so the + /// tokens a WHOLE-BLOCK fallback discards are distinguishable from an + /// ordinary top-level resync. Both call the same function. + in_bdd_fallback: bool, } #[derive(Clone)] @@ -1155,6 +1166,8 @@ impl Parser { bdd_role_preset: false, bdd_first_col_preset: None, dropped_spans: Vec::new(), + dropped_channels: Vec::new(), + in_bdd_fallback: false, } } @@ -1263,6 +1276,7 @@ impl Parser { if self.dropped_spans.len() < 20000 { self.dropped_spans .push((self.current.line as u32, self.current.lexeme.clone())); + self.dropped_channels.push("brace-body"); } self.advance(); } @@ -1330,6 +1344,7 @@ impl Parser { if self.dropped_spans.len() < 20000 { self.dropped_spans .push((self.current.line as u32, self.current.lexeme.clone())); + self.dropped_channels.push("clause-junk"); } if self.current.kind == TokenKind::LBrace { self.advance(); @@ -1425,6 +1440,14 @@ impl Parser { if self.dropped_spans.len() < 20000 { self.dropped_spans .push((self.current.line as u32, self.current.lexeme.clone())); + // W699: `restore_bdd_fallback` resyncs through this same + // function, and "a whole braceless block fell back" is a + // different finding from "a top-level item was skipped". + self.dropped_channels.push(if self.in_bdd_fallback { + "bdd-block-fallback" + } else { + "top-level-resync" + }); } self.advance(); } @@ -1551,6 +1574,7 @@ impl Parser { if self.dropped_spans.len() < 20000 { self.dropped_spans .push((self.current.line as u32, self.current.lexeme.clone())); + self.dropped_channels.push("stray-brace"); } self.advance(); self.parse_module_body(&mut module)?; @@ -2993,8 +3017,36 @@ impl Parser { // spelled as a fn (linker.t27). Detect BEFORE return-type parsing, // which would otherwise consume `given` as an identifier return type. if self.current.kind == TokenKind::Ident && self.current.lexeme == "given" { - self.skip_to_next_top_level(); - return Ok(decl); + // W699 rung 5: this arm RECOGNISED the shape by name and then threw + // it away. `skip_to_next_top_level()` discarded every clause under + // such a fn -- 2 453 tokens across 19 specs, and `given` is the + // fourth-largest head token in the whole corpus discard. + // + // The shared clause parser already serves `test`, `invariant` and + // `bench`; a fn spelled as a test is the same body. Detection is + // unchanged -- same token, same lexeme -- only the action is. + // + // The column anchor is what the bench path (W905) had to set for the + // same reason: continuation statements need an anchor that the head + // never established, and without it the statement arms stay dark. + // ... and it is lowered as a TEST, not as a function. + // + // The first attempt kept the FnDecl and filled its body. Every + // backend then treated it as a real function: `gen-verilog` emits + // synthesizable RTL for functions and deliberately does NOT lower + // tests, so the recovered clauses became `\assert (...)` inside a + // task -- "Enable of unknown task ``assert''" -- and the elaboration + // ratchet caught it, linker 4 -> 6. Correctly: a task body cannot + // assert, and a test body must not become one. + // + // `fn name() given ... then ...` IS a test. Emitting a TestBlock + // teaches no backend anything new: each already knows whether it + // lowers tests, and each now does the right thing with this one. + let mut block = Node::new(NodeKind::TestBlock); + block.name = decl.name.clone(); + self.bdd_first_col_preset = Some(self.current.col); + self.parse_bdd_clauses(&mut block); + return Ok(block); } // Optional arrow for return type: -> Type @@ -3296,6 +3348,7 @@ impl Parser { if self.dropped_spans.len() < 20000 { self.dropped_spans .push((self.current.line as u32, self.current.lexeme.clone())); + self.dropped_channels.push("stmt-recovery"); } } match self.current.kind { @@ -6545,7 +6598,13 @@ impl Parser { } block.children.truncate(start_children); self.restore_state(entry); + // W699: nested fallbacks are possible, so save and restore rather than + // clearing -- an inner block finishing must not tell the outer one's + // remaining tokens they came from a plain resync. + let outer = self.in_bdd_fallback; + self.in_bdd_fallback = true; self.skip_to_next_top_level(); + self.in_bdd_fallback = outer; } fn parse_invariant_block(&mut self) -> Result { @@ -19342,6 +19401,38 @@ impl Compiler { Ok((ast, parser.dropped_top_level_tokens())) } + /// W699: the discarded tokens with the recovery that threw each away, as + /// `(line, lexeme, channel)`. + /// + /// The channel vector is pushed in lockstep with the spans. If the two + /// lengths ever disagree this REFUSES rather than zipping to the shorter -- + /// see the note at the check. + pub fn parse_ast_dropped_records(source: &str) -> Result, String> { + let lexer = Lexer::new(source); + let mut parser = Parser::new(lexer); + let _ = parser.parse()?; + // W699: `zip` truncates to the shorter side, and that is exactly how a + // missed push site hides. Two sites WERE missed on the first pass -- 27 + // tokens across 27 specs -- and the only reason it surfaced was a total + // that did not match `parse-complete`'s. Refuse instead of truncating. + if parser.dropped_spans.len() != parser.dropped_channels.len() { + return Err(format!( + "drop accounting is inconsistent: {} span(s) but {} channel(s). \ + A recovery site records a span without naming its channel; find \ + it rather than reading the shorter list.", + parser.dropped_spans.len(), + parser.dropped_channels.len() + )); + } + Ok(parser + .dropped_spans + .iter() + .cloned() + .zip(parser.dropped_channels.iter().copied()) + .map(|((l, x), c)| (l, x, c)) + .collect()) + } + /// W634: the discarded tokens themselves, as `(line, lexeme)`. pub fn parse_ast_dropped_spans(source: &str) -> Result, String> { let lexer = Lexer::new(source); diff --git a/bootstrap/src/main.rs b/bootstrap/src/main.rs index 4caae52428..7447138f26 100644 --- a/bootstrap/src/main.rs +++ b/bootstrap/src/main.rs @@ -487,6 +487,15 @@ enum Commands { #[arg(long)] show: Option, + /// W699: group the whole corpus's discard by the token the parser + /// STOPPED ON -- the head of each contiguous dropped run. + /// + /// A ranked list says where the tokens are and a keyword match over the + /// traces guesses why. This asks the record itself: the parser wrote + /// down every token it threw away, and the first one of each run is the + /// construct it could not read. Nothing is inferred. + #[arg(long, default_value_t = false)] + causes: bool, /// Name the top-level items whose removal changes the discard count. /// /// `--show` prints WHAT was dropped; this says WHICH construct the @@ -3937,11 +3946,40 @@ fn run_bisect(path: &str) -> anyhow::Result<()> { Ok(()) } +/// Contiguous runs of dropped tokens, as `(head lexeme, token count)`. +/// +/// A run breaks at a line gap: the spans carry a line but no column, so two +/// dropped regions on the same line are indistinguishable from one, and a blank +/// or surviving line between them is the only separator available. That is a +/// deliberate under-count of runs, never an over-count -- it can merge two +/// causes into one, and cannot invent a cause that is not there. +fn dropped_runs(records: &[(u32, String, &'static str)]) -> Vec<(String, &'static str, usize)> { + let mut runs: Vec<(String, &'static str, usize)> = Vec::new(); + let mut prev: Option<(u32, &'static str)> = None; + for (line, lex, chan) in records { + // A run continues only while BOTH hold: the lines are adjacent and the + // recovery is the same one. Two channels meeting on consecutive lines + // are two findings, and merging them would attribute one's tokens to the + // other's head. + match prev { + Some((p, c)) if *line <= p + 1 && c == *chan => { + if let Some(last) = runs.last_mut() { + last.2 += 1; + } + } + _ => runs.push((lex.clone(), *chan, 1)), + } + prev = Some((*line, *chan)); + } + runs +} + fn run_parse_complete( specs_dir: &str, include_scratch: bool, show: Option<&str>, bisect: Option<&str>, + causes: bool, ) -> anyhow::Result<()> { if let Some(path) = bisect { return run_bisect(path); @@ -3992,6 +4030,75 @@ fn run_parse_complete( } } files.sort(); + + // W699: what the parser STOPPED ON, corpus-wide. + // + // The classification this replaces was a keyword match over the printed + // traces, run from outside the compiler -- it guessed `forall` from the + // presence of the word. This asks the record: the head of each contiguous + // dropped run IS the token recovery began at. `forall` is not the answer it + // gives, and the answer it gives is better. + if causes { + let mut runs_by_head: std::collections::BTreeMap = + std::collections::BTreeMap::new(); + let mut specs_by_head: std::collections::BTreeMap> = + std::collections::BTreeMap::new(); + let mut unread = 0usize; + for f in &files { + let Ok(src) = std::fs::read_to_string(f) else { + unread += 1; + continue; + }; + // A file that does not parse at all has no drop record to read -- + // and it is the `parse` phase's business, not this one. + let Ok(records) = compiler::Compiler::parse_ast_dropped_records(&src) else { + continue; + }; + if records.is_empty() { + continue; + } + for (head, chan, n) in dropped_runs(&records) { + let key = format!("{chan:<19} {head}"); + let e = runs_by_head.entry(key.clone()).or_insert((0, 0)); + e.0 += 1; + e.1 += n; + specs_by_head + .entry(key) + .or_default() + .insert(f.display().to_string()); + } + } + let mut rows: Vec<_> = runs_by_head.iter().collect(); + rows.sort_by(|a, b| b.1 .1.cmp(&a.1 .1).then(a.0.cmp(b.0))); + println!("--- what the parser stopped on ---"); + println!(); + println!(" {:>8} {:>6} {:>6} channel head token", "tokens", "runs", "specs"); + for (head, (runs, toks)) in &rows { + println!( + " {:>8} {:>6} {:>6} {}", + toks, + runs, + specs_by_head[*head].len(), + head + ); + } + println!(); + println!( + " {} distinct head token(s), {} run(s), {} token(s)", + rows.len(), + rows.iter().map(|(_, (r, _))| r).sum::(), + rows.iter().map(|(_, (_, t))| t).sum::() + ); + if unread > 0 { + println!(" {unread} file(s) could not be read -- NOT counted as anything"); + } + println!(); + println!(" A run breaks at a LINE GAP. The spans carry a line and no column, so"); + println!(" two dropped regions on one line read as one: this under-counts runs and"); + println!(" cannot invent a cause that is not there."); + return Ok(()); + } + let (mut ok, mut truncated, mut rejected) = (0usize, 0usize, 0usize); let (mut discarded, mut discarded_tokens) = (0usize, 0usize); for f in &files { @@ -10665,8 +10772,14 @@ async fn main() -> anyhow::Result<()> { } Commands::LexDropped { specs_dir } => run_lex_dropped(&specs_dir)?, Commands::ParseConform => run_parse_conform()?, - Commands::ParseComplete { specs_dir, include_scratch, show, bisect } => { - run_parse_complete(&specs_dir, include_scratch, show.as_deref(), bisect.as_deref())? + Commands::ParseComplete { specs_dir, include_scratch, show, bisect, causes } => { + run_parse_complete( + &specs_dir, + include_scratch, + show.as_deref(), + bisect.as_deref(), + causes, + )? } Commands::CheckCalls { specs_dir, include_scratch } => { run_check_calls(&specs_dir, include_scratch)? @@ -11071,8 +11184,14 @@ fn main() -> anyhow::Result<()> { } Commands::LexDropped { specs_dir } => run_lex_dropped(&specs_dir)?, Commands::ParseConform => run_parse_conform()?, - Commands::ParseComplete { specs_dir, include_scratch, show, bisect } => { - run_parse_complete(&specs_dir, include_scratch, show.as_deref(), bisect.as_deref())? + Commands::ParseComplete { specs_dir, include_scratch, show, bisect, causes } => { + run_parse_complete( + &specs_dir, + include_scratch, + show.as_deref(), + bisect.as_deref(), + causes, + )? } Commands::CheckCalls { specs_dir, include_scratch } => { run_check_calls(&specs_dir, include_scratch)? diff --git a/bootstrap/src/parse_conform.rs b/bootstrap/src/parse_conform.rs index 75ae8c7df5..c4b6bb0b56 100644 --- a/bootstrap/src/parse_conform.rs +++ b/bootstrap/src/parse_conform.rs @@ -231,6 +231,14 @@ version of this is the parse-no-discard suite phase.", discards: Some(0), note: "`setup` is an Ident, so it was read as a CLAUSE HEAD and its argument list as the clause's value; the lowering failed and the whole block fell to the discard, taking the assertion after it. specs/isa/ternary_deque.t27 lost 1873 tokens this way -- and the calls are what SET UP the state the assertions check", }, + Case { + name: "a_fn_spelled_as_a_test_keeps_its_clauses", + input: "module m\n\nfn g(x: u32) -> bool { return x == 0; }\n\n fn plain_test()\n given a = 1\n then g(a) == false\n", + verdict: Verdict::Full, + decls: Some(2), + discards: Some(0), + note: "the arm RECOGNISED this shape by name -- `fn name() given ...` -- and then called skip_to_next_top_level on it, throwing away every clause. The shared clause parser already serves test, invariant and bench; detection is unchanged, only the action is", + }, Case { name: "unterminated_fn_body", input: "module m\n\nfn a() -> u32 { return 1;\n", diff --git a/bootstrap/stage0/FROZEN_HASH b/bootstrap/stage0/FROZEN_HASH index 736b8d5baf..54e51dafb0 100644 --- a/bootstrap/stage0/FROZEN_HASH +++ b/bootstrap/stage0/FROZEN_HASH @@ -1 +1 @@ -3e563db2d411526ac9be21f36434924158ae0d68b271c5b8deac08873fb80886 +fcfb279c055ccb603ec8eea758053347198a27ce01baa7d6c5240a961d7af697 diff --git a/cli/tri/src/discard.rs b/cli/tri/src/discard.rs index 5605920a95..f188a1e8ef 100644 --- a/cli/tri/src/discard.rs +++ b/cli/tri/src/discard.rs @@ -29,28 +29,29 @@ pub enum DiscardCmd { #[arg(long, default_value_t = 15)] n: usize, }, - /// Group the discard by what the parser stopped on. + /// Group the discard by which recovery threw it away, and what it 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. + /// Reads `t27c parse-complete --causes`, which reports the PARSER's own + /// record. The keyword heuristic this replaced guessed `forall` from the + /// presence of the word; the record says 78% of the discard is one channel, + /// a whole braceless block falling back, and that `given` -- the head that + /// named the fn arm fixed in rung 5 -- owed only 43 of its 2 453 tokens to + /// it. Head token and recovery channel are different questions. 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"]), -]; +// W699 rung 6: this used to be a keyword match over printed traces, run from +// outside the compiler. It guessed `forall` from the presence of the word. +// +// It no longer guesses. `t27c parse-complete --causes` reports what the PARSER +// recorded: which of five recovery channels threw each token away, and the head +// of each contiguous dropped run. The heuristic said "forall 20 991"; the record +// says 78% of the discard is one channel -- a whole braceless block falling back +// -- and the colon after an invariant name is the largest single head. +// +// The old buckets are gone rather than kept as a cross-check. Two answers to one +// question is what #2767 is about, and a heuristic beside a reading is the same +// shape one level down. fn repo_root() -> Result { let out = std::process::Command::new("git") @@ -131,72 +132,38 @@ 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 { +fn classify(root: &std::path::Path) -> Result<()> { let t27c = ["target/release/t27c", "target/debug/t27c"] .iter() .map(|p| root.join(p)) - .find(|p| p.is_file())?; + .find(|p| p.is_file()) + .ok_or_else(|| { + anyhow::anyhow!( + "t27c is not built. `cargo build --release -p t27c` first --\n \ + reporting nothing rather than a classification this run did not earn" + ) + })?; let out = std::process::Command::new(t27c) - .args(["parse-complete", "--show", spec]) + .args(["parse-complete", "--causes"]) .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`."); + .context("running `t27c parse-complete --causes`")?; + if !out.status.success() { + anyhow::bail!( + "`t27c parse-complete --causes` exited {}. Nothing is claimed.", + out.status + ); } - 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."); + print!("{}", String::from_utf8_lossy(&out.stdout)); Ok(()) } pub fn run(cmd: &DiscardCmd) -> Result<()> { let root = repo_root()?; - let obs = observed(&root)?; if matches!(cmd, DiscardCmd::Classify) { - return classify(&root, &obs); + return classify(&root); } + let obs = observed(&root)?; let pin = pinned(&root)?; let DiscardCmd::Top { n } = cmd else { @@ -250,32 +217,6 @@ 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-ask-the-parser-do-not-grep-what-it-printed.md b/docs/now/2026-08-29-ask-the-parser-do-not-grep-what-it-printed.md new file mode 100644 index 0000000000..55bf265d09 --- /dev/null +++ b/docs/now/2026-08-29-ask-the-parser-do-not-grep-what-it-printed.md @@ -0,0 +1,8 @@ +# NOW -- Ask the parser, do not grep what it printed (2026-08-29) + +## Ask the parser, do not grep what it printed (Refs #2754) + +- every dropped token now carries the recovery that threw it away: bdd-block-fallback 23852 (78%), brace-body 4602, top-level-resync 1894, stray-brace and stmt-recovery the rest +- head token is not channel: given was the 4th-largest head at 2453 tokens and the fn arm that names it owed only 43 of them +- the fn arm recognised by name and called skip_to_next_top_level on it; the shared clause parser already served test/invariant/bench +- zip over two parallel vectors truncated silently and hid two missed push sites -- 27 tokens; the accessor now refuses on a length mismatch diff --git a/docs/now/2026-08-29-the-elaboration-ratchet-was-right-and-my-ruler-was-wrong.md b/docs/now/2026-08-29-the-elaboration-ratchet-was-right-and-my-ruler-was-wrong.md new file mode 100644 index 0000000000..c441a241fe --- /dev/null +++ b/docs/now/2026-08-29-the-elaboration-ratchet-was-right-and-my-ruler-was-wrong.md @@ -0,0 +1,7 @@ +# NOW -- The elaboration ratchet was right and my ruler was wrong (2026-08-29) + +## The elaboration ratchet was right and my ruler was wrong (Refs #2754) + +- keeping the FnDecl made gen-verilog emit assert inside a task; a fn spelled as a test now parses to a TestBlock and every backend already knows what that is +- I measured with bare iverilog while the gate runs -g2012 -DSIMULATION: two rulers, opposite verdicts about the same file +- elaboration errors back to 176 = baseline, discard unchanged at 30408 diff --git a/docs/reports/suite_expectations.json b/docs/reports/suite_expectations.json index 432d2fc328..ac88cc407c 100644 --- a/docs/reports/suite_expectations.json +++ b/docs/reports/suite_expectations.json @@ -1,7 +1,7 @@ { "schema_version": 1, "generated_by": "t27c suite --bless-expectations", - "max_entries": 178, + "max_entries": 177, "entries": [ { "path": "specs/account/repo.t27", @@ -226,14 +226,6 @@ "issue": 1959, "expires": "2026-11-30" }, - { - "path": "specs/fpga/linker.t27", - "phase": "parse-no-discard", - "reason": "unclassified: blessed by --bless-expectations", - "issue": 1959, - "expires": "2026-11-30", - "discard_tokens": 43 - }, { "path": "specs/fpga/mac.t27", "phase": "parse-no-discard",