Skip to content

feat: allow ignoring individual style linter errors; rewrite update-style-exceptions in Lean#14273

Closed
grunweg wants to merge 22 commits intomasterfrom
MR-pretty-linter-output
Closed

feat: allow ignoring individual style linter errors; rewrite update-style-exceptions in Lean#14273
grunweg wants to merge 22 commits intomasterfrom
MR-pretty-linter-output

Conversation

@grunweg
Copy link
Copy Markdown
Contributor

@grunweg grunweg commented Jun 30, 2024

  • add an --update flag to just add exceptions for all current errors
    (People have asked for this since the "file length linter" was created; now it's easily possible!)
  • reimplement the update-style-exceptions script in Lean, as lean 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).


Open in Gitpod

grunweg added 5 commits June 30, 2024 02:57
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.
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jun 30, 2024

PR summary f6ae96aac5

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ ErrorContext.isCoveredByExceptions
+ ErrorContext.isSimilar
+ OutputSetting
+ lintModules
- instance : BEq ErrorContext
- lintAllFiles

You can run this locally as follows
## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

@grunweg
Copy link
Copy Markdown
Contributor Author

grunweg commented Jun 30, 2024

@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
Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why is the flag called --regenerate and not --update as in lake exe shake --update?

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

So --regenerate is the same as "delete nostyle" + --update, right? Maybe it doesn't need to exist as a separate flag

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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)

Copy link
Copy Markdown
Contributor Author

@grunweg grunweg Jul 9, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

That will be more implementation work: but indeed, that is possible.

@grunweg grunweg added the awaiting-author A reviewer has asked the author a question or requested changes. label Jul 9, 2024
@ghost ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 10, 2024
@grunweg
Copy link
Copy Markdown
Contributor Author

grunweg commented Jul 12, 2024

#14697 has a rewrite of these changes: closing this PR in favour of that one.

mathlib-bors bot pushed a commit that referenced this pull request Jul 13, 2024
To prepare for #14273; pulled out for easy of reviewing.
Commits can be reviewed individually.



Co-authored-by: Kim Morrison <kim@tqft.net>
@grunweg grunweg added blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Aug 1, 2024
@ghost ghost removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Aug 2, 2024
@ghost
Copy link
Copy Markdown

ghost commented Aug 2, 2024

This PR/issue depends on:

@grunweg
Copy link
Copy Markdown
Contributor Author

grunweg commented Aug 2, 2024

Closing, as #14697 has landed now.

@grunweg grunweg closed this Aug 2, 2024
@grunweg grunweg deleted the MR-pretty-linter-output branch August 2, 2024 10:01
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) t-linter Linter

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants