style exceptions linter

Stream: mathlib4

[David Loeffler]

I gather there have been some changes recently to the "style linter" mechanism (particularly the part of it that checks for over-long files). I'd like to point out that some of the error messages, and the scripts to fix errors, seem not to have been updated for this change.

More precisely: for recording which files are known to exceed the 1500-line length limit, the "old" mechanism was to maintain a list in scripts/style_exceptions.txt; @Damiano Testa's PR #15610 changed this so the "new" mechanism is to add a line set_option linter.style.longFile xxx to the offending file.

So, I had a PR (#13997) which failed to build because of this; and the CI output from the linter gave the following message:

error: Mathlib/Data/ZMod/Basic.lean:1: file contains 1505 lines, try to split it up error: found 1 new style error(s) run `lake exe lint-style --update` to ignore all of them

So I ran lake exe lint-style --update, and the error in CI went away, so I thought everything was OK. However (as @Jeremy Tan fortunately spotted), the update script had applied the old exceptions mechanism (adding a line to scripts/style_exceptions.txt), not the new one.

Did someone forget to update lint-style --update? Or did the problem arise because I was running lake exe lint-style --update within a branch based on a pre- #15610 master, and the problem goes away for PR branches based on more recent master versions? If it's the latter, then the problem will go away with time, but it's possible that others might still get bitten in the meantime.

[Damiano Testa]

The new linter, the syntax-based one, will complain in the file itself and suggests to use set_option .... The command-line version is just for the old version, that should be removed soon from mathlib (or maybe has already been removed).

The eventual form should be to only have the syntax linter and copy-pasting the "correct" set_option from the linter's message.

I'll ping @Michael Rothgang, since he is more knowledgeable of the "text-based" linters.

[David Loeffler]

Damiano Testa said:

The new linter, the syntax-based one, will complain in the file itself and suggests to use set_option .... The command-line version is just for the old version, that should be removed soon from mathlib (or maybe has already been removed).

By "in the file itself", do you mean "when the file is open for editing in VSCode"?

In this particular case, there was never a time when the file was open in VSCode and over-long, because the combination of additions from two separate PR's took the file concerned over the length limit – not either PR individually. So for the file-length linter, it's crucial that it does get executed on every file (or, at least, every modified file) as part of the CI cycle, and that the warnings / suggestions it produces when run in this mode are not misleading.

EDIT. Hold it, I understand what is going on now. The issue is that both linters exist in parallel at the moment, and both of them get fired up during CI; but the old (purely text-based) linter gets executed much earlier in the CI cycle since it doesn't require a complete build first. So the "run failed" notification from Bors only relayed the error message from the old linter, because it apparently only reports the first failing CI step. The error message from the new one, with directions for adding the exception in the new way, is also there in the CI logs, but got "masked" by the earlier report from the old text-based linter. So the problem I'm reporting can be solved simply by killing the old text-based line-length linter.

[Damiano Testa]

I think that your analysis is correct and I also think that overnight the text-based linter was removed. :smile:

[Michael Rothgang]

I think you figured it out already: to clarify and summarise,

• the old text-based linter used scripts/style-exceptions.txt; the new syntax-based linter uses set_option linter.style.longFile ...
• there was a brief time window when both linters were on master. Your PR created an overly long file during this time window, so both linters would apply...
• the text-based linter has been removed now, so this issue has been resolved.

Sorry for the inconvenience!

[Bryan Gin-ge Chen]

@Michael Rothgang Do we need to do anything with the update-nolints workflow or was that also updated along with the recent changes?

[Michael Rothgang]

I think the update-nolints workflow should continue to work: the lint style --update step will do nothing in practice, as there are no exceptions in that file any more.

[Michael Rothgang]

I have considered removing style-exceptions.txt altogether: that would of course require an update to the workflow. (Let me ask about that in a different topic. Edit: go here)