Long lines linter regression

Stream: mathlib4

[Yaël Dillies]

@Damiano Testa, @Michael Rothgang (I think you are the relevant persons?), the new style linter for long lines has a pretty serious (IMO) regression in behavior compared to the old one: Since it generates warnings during the build, and the mathlib build errors on warnings, we don't get all the long line errors in the build at once, meaning that one needs to spend several CI cycles to shorten lines when previously all long lines were flagged simultaneously and could be fixed at once.

[Yaël Dillies]

This just bit me in #15177

[Damiano Testa]

I was also thinking of adding back the old linter anyway, since the linter only flags long lines after the linter starts to be imported. Let me PR it back.

[Damiano Testa]

The only drawback that I see with the two linters working, is that exceptions need to be recorded twice. Since there is currently exactly one exception in Mathlib, this does not seem too onerous.

[Damiano Testa]

#15190

[Sebastian Ullrich]

Since it generates warnings during the build, and the mathlib build errors on warnings, we don't get all the long line errors in the build at once

@Yaël Dillies Which CI run is this? lake build --wfail should not fail on warnings until the very end

[Yaël Dillies]

Sorry, not at a computer right now but it's somewhere in #15177