feat: allow ignoring individual style linter errors; rewrite update-style-exceptions in Lean#14273
feat: allow ignoring individual style linter errors; rewrite update-style-exceptions in Lean#14273
update-style-exceptions in Lean#14273Conversation
Instead of the current mix of two Python and one shell scripts, just have one lake executable called with different options. While there are still python style linters, we need a way to call those: replace the update-style-exceptions script by a more minimal script, named print-style-errors. This serves as additional incentive to change workflows.
PR summary f6ae96aac5Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
|
@adomani @semorrison @YaelDillies Would one of you like to review another "rewrite Python style linters" PR? |
| run: | | ||
| env LEAN_ABORT_ON_PANIC=1 lake exe runLinter --update Mathlib | ||
| ./scripts/update-style-exceptions.sh | ||
| lake exe lint_style --regenerate |
There was a problem hiding this comment.
Why is the flag called --regenerate and not --update as in lake exe shake --update?
There was a problem hiding this comment.
I considered that --- note that I defined two flags, --update and --regenerate.
The former only ignores new errors: this is suitable when you e.g. don't want to split a file which your change pushed over the limit. The latter regenerates all exceptions; in practice, this will incur more churn since the current number of lines is encoded in the file... so, to me only making the latter change occasionally (but not as a side effect) to intentional.
With shake, --update corresponds to my --regenerate, so is a super-set of this.
In terms of consistency, I think this is fine: the default action should be to call --update; not --regenerate. (If I get around to fixing the nolints bot, the file will be regenerated once a week.)
I could rename --update to --ignore if this is clearer; perhaps even with an error on using --update to clarify the distinction.
There was a problem hiding this comment.
So --regenerate is the same as "delete nostyle" + --update, right? Maybe it doesn't need to exist as a separate flag
There was a problem hiding this comment.
Yup. But then, why did we have update-style-exceptions.py? Or, put differently, how are we going to remove entries from the list? Automatically updating seems useful enough (to expert users) to make it low-friction; it just doesn't need to be the first operation users are exposed to.
There was a problem hiding this comment.
Well you are worried about unnecessarily updating existing entries, not about correctly removing redundant entries, right? So --update could
- Recompute the file
- Add the lines to be added
- Remove the lines to be removed
- Not touch the lines that are merely modified (so long as not touching them is not causing a linting error)
There was a problem hiding this comment.
That will be more implementation work: but indeed, that is possible.
just pass one big collection of modules to the core script.
use an explicit method for fuzzy comparison instead
|
#14697 has a rewrite of these changes: closing this PR in favour of that one. |
To prepare for #14273; pulled out for easy of reviewing. Commits can be reviewed individually. Co-authored-by: Kim Morrison <kim@tqft.net>
|
This PR/issue depends on:
|
|
Closing, as #14697 has landed now. |
(People have asked for this since the "file length linter" was created; now it's easily possible!)
update-style-exceptionsscript in Lean, aslean exe lint_style --regenerate.As long as there are Python style linters, this calls into the Python linters to update the output.
(In effect, this PR flips the call responsibility: now the Lean code calls the Python code, not vice versa.)
This simplifies the style linter infrastructure: two shell and one python script are replaced by one Lean executable and one Python script (which ought to be transient, and disappear when all Python linters are rewritten).
Rebased and cleaned up version of feat: prettier output on style errors #13623. Commits can be reviewed individually.