-
Notifications
You must be signed in to change notification settings - Fork 331
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
refactor(lint-style): various small clean-ups #12596
Conversation
I'm not sure I agree with the first commit: if the script can produce an error, we should be able to except it |
I see your point, but I would argue that the particular errors I'm removing should never land in mathlib anyway - so I don't see why excepting them would be useful! (If there's the need to make the build pass, commenting that linter is another option.) (FWIW, the script currently doesn't implement excepting all errors, so the current logic is already different.) |
894c13c
to
fce04ec
Compare
I pushed a few more commits, refactoring the script further: in particular, parsing style-exceptions now truly recognises all possible errors, in fewer lines of code than before. |
1f7eaff
to
25bb22e
Compare
This allows simplifying format_errors further: for an enum value v, v.name outputs the corresponding variant name.
cb3bf5a
to
4ab0d78
Compare
@@ -65,20 +68,12 @@ | |||
for exline in f: | |||
filename, _, _, _, _, errno, *extra = exline.split() | |||
path = ROOT_DIR / filename | |||
if errno == "ERR_COP": |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This removes some variants; a later commit implements parsing all exception types (making this obsolete).
(I didn't feel like editing history again to edit this part out.)
Let me close this PR in favour of #13199 (and its pieces). |
See individual commit messages for details. Each commit can be reviewed independently.