fix: correct behavior of runLinter --update
#1600
Open
Conversation
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
github-actions
bot
added
the
awaiting-review
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Jan 5, 2026
Contributor
Author
|
WIP |
github-actions
bot
added
WIP
Contributor
Author
|
On zulip, it was mentioned that the current behavior for adding new violations to the nolint file is also useful (or possibly the primary use case!). (Note that the current behavior still needs a tweak because it overeagerly erases nolints that are not from the current module.) I think both functionalities have a place; maybe |
Collaborator
|
Mathlib CI status (docs):
|
leanprover-community-mathlib4-bot
added
the
merge-conflict
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 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.
This PR changes the behavior of
runLinter --update. Previously, this would overwrite the nolints.json file with the full list of current linting violations, meaning that all declarations which violated linters were now nolinted.However, it is intended to only "remove any declarations that no longer need
to be nolinted" (at least according to the docstring). This means that we should just filter out declarations from the nolints file which no longer fail (i.e., only include those from the nolints file which do still fail).
Since technically we run linters on individual modules, but the nolints.json file may apply to other modules besides the one being linted, we also only filter out those newly non-failing declarations which are from the current module and therefore are actually being linted.
This extra check can introduce some potential (benign) staleness in nolints.json if a nolinted declaration is removed (and thus never appears in any module, and so is never removed by
--update). However, these ineffective nolints will not cause any problems, while overzealously deleting nolints from other modules might.In the future, we might want to consider factoring out the
--updatebehavior so that it is not part ofrunLinterOnModule, but instead occurs at the top level inmain.If possible, I'd like someone to verify that this is indeed the intended behavior of
--update, and that it's not the case that the docstring is wrong. :)