Repository navigation
feat(frontier): --watch skips a spec whose four gen hashes did not change - #10247
Merged
Merged
Conversation
…ange (Closes #10237) The watch loop reran every spec whose closure digest moved, and the digest hashes source text: a comment or a blank line moves it while the Zig, Verilog, C and Rust outputs stay byte-identical, so the rerun (about 2 s) could not change the verdict. specs/verified/watch.t27 gains watch_skip(recorded, computable, same_gen), with tests and a negative control: a spec with no recorded or no computable gen hashes is rerun (fail open to a rerun, never to silence). The loop records each spec's four gen hashes (gen_cached, the cache the digest already keys) at the first look and after every rerun, and supplies the three booleans. A skipped spec still has its digest recorded, so the next look does not see it as changed again. The hand-written Rust is net zero lines (4 added, 4 deleted). Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
Contributor
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Closes #10237
Epic #8095 (hot reload), ledger #8737. Second step of the change-only inner loop.
What changes
specs/verified/watch.t27gainswatch_skip(recorded, computable, same_gen)(2 new tests incl. a negative control, 1 new invariant; 5 tests + 2 invariants in all, 0 vacuous). A spec whose closure digest moved is skipped only when its four gen hashes (Zig, Verilog, C, Rust) were recorded, are computable now, and are unchanged. No recorded or no computable gen hashes means a rerun: fail open to a rerun, never to silence.run_frontiersupplies the three booleans fromgen_cached, the cache the digest already keys. It records the four gen hashes of every spec at the first look and of each spec after its rerun. A skipped spec still has its digest recorded, so the next look does not see it as changed again.bootstrap/src/service.rs(every edit is folded into an existing line).bootstrap/src/test_report.rsis untouched.bootstrap/gen/rust/verified/watch.rsand resealed.trinity/seals/verified_VerifiedWatch.json.Checked on the Railway lab
t27c test-report specs/verified/watch.t27: 5 of 5 pass, 0 vacuous.frontier --listbefore vs after the reseal differs only in1 specs/verified/watch.t27(now REUSE) and the matching totals; no other line moves.frontier --watch, appending a comment word to a header line ofwatch.t27: silent for 12 s. Changingreturn digest_changed;toreturn digest_changed == true;:ok specs/verified/watch.t27: 5 of 5 passprinted.🤖 Generated with Claude Code