feat(FormalConjecturesUtil): linter for answer(sorry) in solved statements - #5077
Open
theebayuser wants to merge 2 commits into
Open
feat(FormalConjecturesUtil): linter for answer(sorry) in solved statements#5077theebayuser wants to merge 2 commits into
theebayuser wants to merge 2 commits into
Conversation
…tatements Adds `linter.style.category_answer`, which warns when a declaration tagged `@[category research solved]` still uses `answer(sorry)`. The check is syntactic: under the default `google.answer` setting `answer(sorry)` at `Prop` elaborates to a bare `True`, so the placeholder is not visible in the elaborated term. The shared `toCategorySyntax`/`toCategories` helpers move from CategoryDocstringLinter into Attributes/Basic so both linters use them. Eight statements that deliberately keep the placeholder opt out with `set_option linter.style.category_answer false in`, each with a comment saying why: independence of ZFC (1119, 1175), constants that are not known explicitly (416, twice, and 975), question-form headlines whose answer is recorded in a variant (1007, 1026), and a TODO in GraphConjecture34.
github-actions
Bot
added
documentation
mo271
reviewed
Aug 21, 2026
mo271
left a comment
mo271
left a comment
Collaborator
There was a problem hiding this comment.
LGTM, thanks!
left some comments
…ts, trim test and docs)
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
2 participants
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.
follow-up pr to #4965: a linter that catches the
answer(sorry)placeholders thatPR fixed by hand. Part of #1407.
linter.style.category_answerwarns when a declaration tagged@[category research solved]still writes
answer(sorry). The check has to be syntactic: under the defaultgoogle.answersetting,
answer(sorry)atPropelaborates to a bareTrue, so by the time the term existsthe placeholder is gone. It scans the whole
declSig, so it also catches value-positionanswers such as
IsGreatest S answer(sorry), not justanswer(sorry) ↔ ….This is the category-aware complement to #1958's
AnswerLinter, which checks quantifierscoping but does not read the category.
The shared
toCategorySyntax/toCategorieshelpers move fromCategoryDocstringLinterintoAttributes/Basicso both linters use them.Eight statements deliberately keep the placeholder and opt out with
set_option linter.style.category_answer false in, each with a comment giving the reason:independence of ZFC (1119, 1175), constants not known explicitly (416, twice, and 975),
question-form headlines whose answer is recorded in a variant (1007, 1026), and a TODO in
GraphConjecture34.Off by default; enabled repo-wide through
weak.linter.style.category_answerinlakefile.toml, matching how the other style linters are switched on.A repo-wide scan found no
research solveddeclaration with a survivinganswer(sorry)beyond those eight.
lake --wfail build FormalConjecturesForMathlib FormalConjecturesUtil— clean (8064 jobs)lake --wfail test— the newFormalConjecturesTest/Util/Linters/CategoryAnswerLinter.leanpins both the firing and the silent cases with
#guard_msgsNegative control: temporarily removing one opt-out makes the linter fire at the expected
line, and restoring it silences the warning again