A whitespace linter

Stream: mathlib4

[Damiano Testa]

#24465 contains a linter that enforces whitespace formatting on all declarations up to and excluding the type signature. Essentially, it checks that the "hypotheses" of each declaration are correctly formatted.

[Damiano Testa]

While the scope is limited, the linter found hundreds of exceptions in mathlib, including one in #24119, merged 8 hours ago.

[Damiano Testa]

The PR is long, but a lot of it is documentation, tests and making the tests compliant. All the mathlib adaptation PRs that resulted from it have been completely straightforward.

[Damiano Testa]

Another strong point in favour of the linter is that it has no "special-casing", although it has an exclusion mechanism to allow the linter to ignore parts of a declaration, based on the syntax type that gave rise to them.

[Damiano Testa]

Overall, I think that it works very well and the fact that there isn't a single exception in all of mathlib seems a strong endorsement!

[Damiano Testa]

Some previous discussions:

• #mathlib4 > Linting space around variables
• #general > Mathlib community meetings @ 💬

[Michael Rothgang]

As I already said on github (also perhaps on a related PR), I think this is great to have. I look forward to extending this linter in the future, towards checking all formatting (with an opt-out for syntax it doesn't understand). I can try to review the linter implementation soon.

[Michael Rothgang]

Let me dream big: what is needed to make this closer to an auto-formatter, i.e. enable the author of a pull request to automatically reformat all affected lines to comply with the linter? I presume there are two steps:

• making the linter generate "try this" suggestions (or similar) --- this is blocked on lean#4363 (the RFC is accepted, I think - and medium priority)
• some way of "apply all try this suggestions in this file" (which could be be useful in many other settings also, such as tryAtEachStep or for auto-fixing all non-terminal simps, and generally for self-rewriting code)

Is there a way to move any of these items forward?

[Michael Rothgang]

(Without opening the can of worms that is lake exe refactor.)

[Damiano Testa]

Right now, the linter piggy-backs on the pretty-printer for deciding what is correctly formatted or not (plus a little custom-handling of where to put line breaks).

[Damiano Testa]

However, the pretty-printer has too many short-comings to be reliably used as an "oracle formatter". This, I view as the main obstacle, and the linter takes no step in this direction.

[Damiano Testa]

The other question, of automated code-editing is certainly (and easily) within reach. I think that all that is lacking is the desire to accept one way as the standard and then build infrastructure around it.

[Damiano Testa]

I ran a few tests, before and after refactor, using it and not using it. They all worked, of course each with its pros and cons.