RFC: remove `scripts/style-exceptions.txt`

Stream: mathlib4

[Michael Rothgang]

The scripts/style-exceptions.txtfile has been recording exceptions to the text-based style linters in lint-style.py and Linter/TextBased. As I understand it, the length of this file is meant to reach zero - and now, it indeed has. :tada:

Some of the linter errors were easy to fix (and just required sustained effort), such some misformatted author lines or missing documentation. The main remaining entries were exceptions for the "long file linter", which has been rewritten as a syntax linter (in #15610 and #16299). Exceptions are now tracked as set_option linter.style.longFile <number> instead, obviating the need for this file.

In my opinion, this impliest the need for file with transient style exceptions is gone. All remaining text-based errors are the following.

• missing or malformatted copyright header; malformatted authors line
• missing module docstring
• broad imports such as "import Mathlib.Tactic"
• the string "adaptation note" (instead of the command #adaptation_note)
• using the wrong kind of cdots (rewriting this as a syntax linter has been bors-approved)
• isolated "by" or "where"; starting a line with a colon; a space before a semicolon
• trailing whitespace or windows line endings
• the second line of a statement is not correctly indented
• a space after "←"
• non-terminal simps

None of these should be introduced in new code; I don't see a reason for keeping an escape hatch for the current linters. Thus, I propose removing style-exceptions.txt.

[Michael Rothgang]

This will simplify the text-based linters quite a bit (just recently, a bug was fixed relating to different path separators).

[Michael Rothgang]

For the curious: there is a file nolints-style.txt which records permanent exceptions to the text-based linters. That file will stay. However, that file must (intentionally) be updated by hand.

[Michael Rothgang]

#16417 removes this file. Needs a PR description (which can be cargo-culted from this thread), and I want to double-check I really caught all references.

[Johan Commelin]

Quite a milestone! Kudos to all the code elves that made mathlib better!

[Yury G. Kudryashov]

Please write a commit message, so that we can merge it.

[Michael Rothgang]

Commit message written

[Bryan Gin-ge Chen]

Just a heads up, there was a missing quote in #16417 which is causing the update nolints job to fail. See #16806