Linting space around variables

Stream: mathlib4

[Damiano Testa]

In the context of one of the items discussed in #general > Mathlib community meetings, #22760 is an attempt to lint "spacing" issues, such as example (a: Nat).

[Damiano Testa]

The linter checks that

• each command starts at the beginning of a line;
• the "hypotheses segment" of each declaration coincides with its pretty-printed version.

[Damiano Testa]

I was somewhat surprised that mathlib is already compliant and the only issues raised by the linter were in a single test file!

[Damiano Testa]

#22766 "fixes" the test file.

[Michael Rothgang]

Damiano Testa said:

I was somewhat surprised that mathlib is already compliant and the only issues raised by the linter were in a single test file!

For those following at home: the truth is sadly more complicated; there are actually a number of violations. (But I would love for them to get fixed.)

[Damiano Testa]

Yes, the reason that I thought that mathlib was complying was that I had forgotten to import the linter... :man_facepalming:

[Damiano Testa]

It looks like a lot of issues come from the fact that the pretty-printer erases comments, so I am hoping that there will be many fewer false positives once I get the linter to erase comments from the source code as well.

[Damiano Testa]

What should the linter do with

instance instPartialOrder : PartialOrder (Fin n) := inferInstance
instance instLattice      : Lattice (Fin n)      := inferInstance

It is hard to make the linter aware of the joint formatting.

[Damiano Testa]

Should these be wrapped inside a set_option linter.commandStart false region?

[Damiano Testa]

Should formatting comply with the linter anyway?

[Michael Rothgang]

Damiano Testa said:

Should formatting comply with the linter anyway?

Personal opinion: consistent formatting and not having to argue about style are huge benefits, so I think we should move towards this goal if we can.

In case there are bikeshedding questions, we decide to make compliance optional (until the bikeshed is somewhat resolved).
If we discover the pretty-printer is really bad in some cases, consciously deactivating the linter seems fine for me.

[Michael Rothgang]

Damiano Testa said:

What should the linter do with

instance instPartialOrder : PartialOrder (Fin n) := inferInstance
instance instLattice      : Lattice (Fin n)      := inferInstance

It is hard to make the linter aware of the joint formatting.

(In a text-based linter, I was thinking of checking these things: if there is a colon which lines up, treat it as conscious alignment, otherwise format normally.)

I believe that "do not align manually" (because this tends to go stale) is the best trade-off in the long term, especially for a diverse project as ours.

[Eric Wieser]

I frequently see column alignment going stale within the evolution of PR, and so the nonstale version never even makes it into mathlib

[Ruben Van de Velde]

I would also prefer not allowing the alignment. Especially when you add a new line where the column would be further to the right, you either get an inconsistency or you needlessly mess up the blame for the other lines

[Damiano Testa]

I am happy to "lint all the way"! I personally have used "whitespace formatting" in my code, but I agree that it is simpler to have a "local" rule for formatting.

[Damiano Testa]

Btw, I'm also testing out a "relative linter", namely one that only lints the code that has been modified, using the git diff as a basis for what counts as "modified".

[Damiano Testa]

If that works, it could be useful to avoid the need of nolints for certain linters, since it would flag an exception during the review process (in a workflow step outside the main CI) and then be silent, if the non-lint-compliant code is accepted nevertheless.

[Damiano Testa]

This can be useful for this specific linter, where there isn't a full set of rules for what is applied.

[Damiano Testa]

So the linter could make suggestions, some of which are "mandatory" others are just optional/up to each contributor's style.

[Damiano Testa]

#22838 is another batch of "fixes", including some "de-formatting" of whitespace alignment.

[Michael Rothgang]

I just maintainer merged. (That doesn't get an emoji, right? - I don't think this is necessarily wrong, but take this as a testament that the emojibot is great :-).)

[Damiano Testa]

That's an interesting idea about emoji reactions for maintainer merges: it would be very easy to add it to the current workflows and makes sense to me.

Feel free to open a PR and/or a discussion about it!

[Michael Rothgang]

#24467 fixes some more whitespace issues in mathlib

[Michael Rothgang]

#24472 fixes some more