Repository navigation
ci: nightly coverage-ledger refresh so a harness change doesn't blank coverage (#4270) - #4625
Merged
Merged
Conversation
… coverage (#4270) evidence-refresh.yml re-sweeps the det ports and rewrites tests/equivalence/det_sweep_coverage.json into the bot PR. Ledger refreshed locally: 26/26 entries were stale (harness+oracle), numbers identical, fingerprints only. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Contributor
squid-protocol
marked this pull request as ready for review
October 7, 2026 16:04
squid-protocol
added a commit
that referenced
this pull request
Oct 7, 2026
…s after #4625 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
squid-protocol
added a commit
that referenced
this pull request
Oct 7, 2026
…ge (#4602) (#4624) * equivalence: cobol_coverage sets apart branch points after a transfer of control (#4602) An IF / EVALUATE no path reaches -- every path to it passes GO TO, GOBACK, STOP RUN, EXEC CICS RETURN / XCTL / ABEND (no RESP / NOHANDLE), or a plain PERFORM of a paragraph no path leaves -- is counted apart (branches.after_transfer), like in_dead_code. A run that takes one is flagged (after_transfer_but_taken). Conservative: conditional phrases, inline PERFORMs, IF with no ELSE, EVALUATE with no OTHER, COPY and Area A lines keep the path open. CardDemo: COCRDLIC 586, COCRDSLC 386, COACTVWC 387; crucible: none. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> * equivalence: a reviewed ledger of infeasible branch outcomes (#4602) tests/equivalence/infeasible_outcomes.json states, per case, the branch outcomes no input can reach, each with its COBOL reason (family G: a guard every caller has satisfied; C: a test of a constant). proof_blockers.py takes them out of the branch total when the proof left them uncovered and prints them; one the proof reached is a gap. Every det sweep fails when a proof reaches a stated outcome (proof_sweep.py keeps each case's uncovered list). infeasible_outcomes.stated(case) is what the evidence report shows as assumptions. First entries: the RETURN-TO-PREV-SCREEN guard (G) in nine CardDemo programs. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> * equivalence: CardDemo scenarios for reachable unrun outcomes, infeasible entries for the rest (#4602) Scenarios (every reachable outcome the harness can express): billpay +9, tranadd +15, report +9, tranlist +11, userlist +11, cardlist +2, cardview +1, userupd +1, userdel +1. Proposed infeasible entries (G / C, each with its COBOL reason): adminmenu 6, menu 3, cardlist 2, cardview 6, report 6, tranadd 2, tranlist 4, userlist 4. Evidence records of the changed cases re-proven (the model ports prove the new scenarios); pages re-rendered. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> * equivalence: track infeasible_outcomes.json (the *.json ignore rule) and test it is tracked (#4602) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> * equivalence: never-raised NOTFND stated (family R); evidence, pages and coverage ledger regenerated (#4602) The REWRITE NOTFND (userupd 377, billpay 390) and DELETE-without-RIDFLD NOTFND (userdel 323) fault scenarios are gone: IBM documents no such response, so the outcomes are stated infeasible under family R, citing IBM's REWRITE / DELETE pages. Evidence records of the 9 changed cases re-proven with evidence.py prove, pages rendered, det_sweep_coverage.json updated from a fresh det sweep (16 cases, all proven). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> * equivalence: det-sweep coverage ledger regenerated for the #4602 cases after #4625 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
This was referenced Oct 7, 2026
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.
Part of #4270.
evidence-refresh.yml(the nightly bot-PR job that re-proves stale evidence records) now also:proof_sweep.py --det-only --skip-db2 --no-ratchet --work $RUNNER_TEMP/sweep(same setup as CI's det-sweep: JDK 17, GnuCOBOL image, pinned corpora already in the job);det_coverage_ledger.py updateon it;tests/equivalence/det_sweep_coverage.jsonto the bot PR'sadd-paths.A failed sweep fails the job at the end (after the PR is opened), like the evidence re-proof.
updatealready rewrote fingerprints from the tree for every proven case (never kept old ones); new testtest_update_rewrites_stale_fingerprintspins that.TODO(#4603):
evidence_report.py --refresh --liveis not on main; a TODO comment names it. #4603 adds that step itself; my hunk sits before "Re-prove the stale records" and the add-paths line is at the top of the list, so the edits should not conflict.Measurement (main 9fd212d)
--refresh --live): programs L0/L1/L2/L3/L4 = 42/41/34/0/0 with the stale ledger -> 42/41/18/13/3 with the refreshed one (16 programs move L2 -> L3/L4: carddemo 13 L3 + 1 L4, cbsa 2 L4).Gates:
pr_gates.py --fast5/5; ledger tests 6 pass. actionlint not available (yaml parses). If #4624 lands first it also touches the ledger: regenerate with the tool, don't merge by hand.🤖 Generated with Claude Code