fix(check-trusted-base): make Lean sorry/axiom matching comment-aware - #532
Merged
Merged
Conversation
The Lean branch stripped only `"string literals"` from a single line before
matching, so it could not see Lean comments -- which nest and span lines. A
docstring that merely MENTIONS `sorry` was therefore reported as a
soundness-relevant escape hatch, and the repo was told to seed
docs/proof-debt.md for a hatch that does not exist.
Found in systemet, whose Audit.lean documents its own policy:
"A theorem that elaborates but smuggles in an axiom or a `sorry` through
an import fails the gate here, not in a status document."
-> [INFO] Found 1 soundness-relevant escape hatch(es).
[ERROR] No docs/proof-debt.md ... but 1 escape hatches exist.
That repo's axiom audit reports [propext, Quot.sound] for all 20 headline
items; there was no hatch. Any repo that documents its own sorry/axiom policy
in a docstring hits this -- i.e. exactly the repos taking the policy most
seriously. The pressure it creates is to declare debt that does not exist,
which is the opposite of what this gate is for.
Fix: strip_lean_noncode() blanks line comments (--), nesting block comments and
docstrings (/- -/, /-! -/, /-- -/) and string literals, preserving line numbers
so reported positions stay accurate. Markers still quote the ORIGINAL line.
Same comment-awareness fix scan-dangerous.sh already carries for Lean.
Failure direction is deliberate: string state is NOT carried across lines, so an
odd quote over-flags rather than blanking the rest of a file. For a soundness
gate, over-flagging is safe; under-flagging is not.
Verified with fixtures -- must catch real holes, must ignore prose:
line 1 /-! docstring ... `sorry` ... -/ NOT flagged (was the bug)
line 2 -- line comment mentioning sorry/axiom NOT flagged
line 3 /- /- nested -/ sorry -/ NOT flagged
line 4 def s : String := "the word sorry ..." NOT flagged
line 5 theorem realHole : True := by sorry FLAGGED
line 6 axiom realAxiom : False FLAGGED
line 7 theorem t : True := by sorry -- trailing FLAGGED
line 8 theorem fine : True := trivial NOT flagged
3 found, all genuine. Before this change the same fixture also reported the
four comment/string lines. `bash -n` clean.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
|
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.
The bug
scripts/check-trusted-base.sh's Lean branch strips only"string literals"from a single line before matching\bsorry\b|^\s*axiom\s. Lean comments nest and span lines, so per-line string stripping cannot see them.Consequence: a docstring that merely mentions
sorryis reported as a soundness-relevant escape hatch, and the repo is told to seeddocs/proof-debt.mdfor a hatch that does not exist.Found in systemet, whose
Audit.leandocuments its own policy:That repo's axiom audit reports
[propext, Quot.sound]for all 20 headline items — there was no hatch. The repos most likely to trip this are the ones documenting the policy most carefully, and the pressure it creates is to declare debt that doesn't exist — the opposite of what this gate is for.The fix
strip_lean_noncode()blanks line comments (--), nesting block comments and docstrings (/- -/,/-! -/,/-- -/) and string literals, preserving line numbers so reported positions stay accurate. Markers still quote the original line text. This is the same comment-awarenessscan-dangerous.shalready carries for Lean.Failure direction is deliberate: string state is not carried across lines, so an odd quote over-flags rather than blanking the remainder of a file. For a soundness gate, over-flagging is safe and under-flagging is not.
Verification — it must still catch real holes
Fixture results (3 found, all genuine):
/-! docstring …sorry… -/-- line comment mentioning sorry and axiom foo/- /- nested block with sorry -/ sorry -/def okString : String := "the word sorry in a string"theorem realHole : True := by sorryaxiom realAxiom : Falsetheorem trailing : True := by sorry -- with trailing commenttheorem fine : True := trivialLine 7 is the important one: code before a trailing comment is still matched, so the stripper cannot be used to hide a real hole behind a comment.
bash -nclean.Because this script gates every proof-bearing repo in the estate, I have not merged it — please review the stripper logic before it goes live.
🤖 Generated with Claude Code