Repository navigation
fix(audits): drop the 2 fixture entries that inline markers now cover - #499
Conversation
#489 added registry entries for the deliberate `sorry` in tests/corpus_fixtures/isabelle/Smoke.thy and tests/corpus_fixtures/minif2f/algebra.lean, because the gate's scanner (panic-attack f2a6a70) could not apply the inline `panic-attack: accepted` markers those files already carry. #497 moved the gate to panic-attack 55ffcc9, which line-anchors Lean and Isabelle `sorry` findings (panic-attack#278), so the markers suppress them. The entries are now a second suppression for the same 2 lines, and they cover every ProofDrift finding in the 2 files, not only the marked line. This removes them; the file returns to its state before #489. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0136P7ZmAsYpFA9gxfQLF3F6 Signed-off-by: Claude <noreply@anthropic.com>
|
Warning Review limit reachedYou've used all free OSS reviews for now. Wait for the free limit to reset to keep reviewing this public repository. Next included review available in 7 minutes. View limit details
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. |
Codex Review Summary: ❌ FailedThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
|
This security review couldn’t start because the paying account has exhausted its Codex allowance and has insufficient available credits. The payer can check their balance and add credits in the Codex usage dashboard, then try again. If you do not manage the paying account, contact this repository's admins. |
|
Summary
PR 489 added 2 entries to
audits/assail-classifications.a2mlfor the deliberatesorryintests/corpus_fixtures/isabelle/Smoke.thyandtests/corpus_fixtures/minif2f/algebra.lean. It needed them because the gate's scanner at the time (panic-attackf2a6a70) could not apply the inlinepanic-attack: acceptedmarkers those files already carry.PR 497 moved the gate to panic-attack
55ffcc9, which anchors Lean and Isabellesorryfindings to their line (hyperpolymath/panic-attack#278). The markers now suppress both findings. So the 2 entries are a second suppression for the same lines. They are also wider than the markers: a registry entry covers every ProofDrift finding in its file, not only the marked line.This PR removes them. The file returns to its exact state before PR 489.
Changes
audits/assail-classifications.a2ml: the 2ProofDriftentries and their comment block are removed (16 lines). No other entry changes.RSR Quality Checklist
Required
unsafeblocks without// SAFETY:comments.envfiles includedAs Applicable
Testing
On a clean checkout of this commit, with the scanner built at
55ffcc9the way the gate builds it (cargo install --git … --rev … --locked --features http):static-analysis-evidence.sh scan panic-attack:status: ran, exit 0. Counts: 0 critical, 43 high, 65 medium, 1 low.static-analysis-evidence.sh gate: exit 0.Smoke.thy:21andalgebra.lean:11(the 2 Criticalsorryfindings):suppressed: true, through their inline markers.One visible change: a Medium ProofDrift finding in
Smoke.thywith no line (the fixture's deliberateaxiomatizationblock) is now counted, so medium goes from 64 to 65. The registry entry used to hide it. The gate blocks only critical findings.Screenshots
Not applicable.
Generated by Claude Code