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.

[Damiano Testa]

Here is another recent whitespace lint: #24585.

[Mario Carneiro]

One thing I would love to have in this vein is something like the vscode typescript formatter. It's very non-judgmental, it doesn't try to do any extra line breaking, and mainly just makes sure that indentation of successive lines is correct and whitespace around operators and parentheses is correct, which means that you get the easy stuff fixed and can leave the harder questions for manual intervention, which seems like a good compromise for a hugely complex syntax like lean's where we want to err on the side of doing something useful but not making a mess

[Martin Dvořák]

Out of curiosity, why is there Symbol in CommandStart.lean?

[Damiano Testa]

Martin Dvořák said:

Out of curiosity, why is there Symbol in CommandStart.lean?

This is a test: at some point, the linter flagged it as an error and I made it into one of the test elements.

[Damiano Testa]

With respect to Mario's comment, the linter implements a very initial step towards that: it verifies whitespace around variables, but trusts line breaks provided by the source code. It also does not provide autocorrection.

[Damiano Testa]

#24664

[Damiano Testa]

Yet more whitespace: #24837.

[Damiano Testa]

Note also that these PRs are all completely automatic: the linter only suggests correct changes :trademark: . In case someone feels like merging it, here is the PR: #24465! :slight_smile:

[Sébastien Gouëzel]

I would love to see the linter in, and active on PRs, because it would save us a lot of boring work when reviewing. Unfortunately, I can't review it for lack of skills, sorry...

[Damiano Testa]

#24946

[Damiano Testa]

I also want to point out what I consider to be an added benefit of this linter: since it actually inspects the pretty-printed version of the various commands, it helps in catching situations where the newly introduced notation would not print accordingly to what you expect. This happened in several of the past PRs, including the one I just linked to.

[Damiano Testa]

I view this as an incremental way of producing a formatter: little by little, the scope of the linter can expand and, each time there is a discrepancy between what has been written and how it pretty-prints, it may mean that there is a style decision to be made about what is the "correct" way of writing a particular part of the syntax.

[Damiano Testa]

#25018

[Damiano Testa]

Dear All,

the whitespace linter has just made its way into mathlib! Essentially, it checks for correct formatting of all declarations up to and excluding the type specification:

theorem X {a : Unit} (b : Nat) :/- end of checking -/ ...

[Damiano Testa]

As usual, with all such new additions, there may be issues: let me know if you run into any unwanted behaviour!

[Kenny Lau]

Are there currently files that violate the linter and could we have a look at an example? Sometimes I'm not sure if things need an extra indentation, like I'll write something like

  very_long_proof_term_1 (moderately_long_proof_term
      the_complement_of_the_moderately_long_proof_term)
    proof_term_2 proof_term_3 proof_term_4

[Damiano Testa]

Specifically indentation is not something that the linter checks, it trusts that you know what you are doing.

[Damiano Testa]

Also, note that it only inspects the hypotheses, so such long terms are rare.

[Damiano Testa]

The main reason for these limitations is that the linter basically uses the pretty-printer as an oracle for formatting, and the pretty-printer is only reliable in a limited setting.

[Damiano Testa]

In fact, while making mathlib compliant, I uncovered several missing spaces in syntax declarations, since no one had ever looked at how they pretty-printed.

[Kenny Lau]

Ah, ok, I had a look at the diff, very interesting, thanks

[Kenny Lau]

image.png

[Kenny Lau]

it looks like this is the only instance where whitespaces issues were identified and fixed?

[Kenny Lau]

ah, and also a few instances of changing notation_class * to notation_class*

[Damiano Testa]

For all (or almost all) the adaptation PRs that I made, I referenced the "linter PR", so they appear as comments. There were a lot of exceptions. Here are some examples.

• #24465 -- the linter
• #24459
• #24467
• #24472
• #24501

and so on.

[Jovan Gerbscheid]

Note that the linter adds 2 minutes of linting time to the mathlib build, according to the speedcenter. Has this been considered and can it be improved?

[Jovan Gerbscheid]

@Damiano Testa, I don't know if the preformance bottleneck is in Lean.PrettyPrinter.ppCategory, Std.Format.pretty or in the implementation of the linter itself. But what I find suspicious is that the linter works with String instead of Substring. This is very memory inefficient, because after every little string token that is being processed, you are allocating memory to copy the whole rest of the String (using String.drop 1). So I would suggest using Substring to avoid this extra memory allocation.

[Michael Rothgang]

I tried doing so in #26240: some of these changes are definitely readability regressions. Let's see if this helps meaningfully...

[Damiano Testa]

Actually, I had initially planned this linter to be a test for a new kind of "relative" linter. However, since there were initially quite a few exceptions and the linter was not the easiest to write, I decided to leave the "relative" part for a later development.

[Damiano Testa]

Now, "relative" refers to the fact that I wanted this linter to only act on the git diff of a PR, and not on all of mathlib. So, the plan is

• write the linter (done);
• make mathlib compliant (done);
• write the code for detecting the git diff and store it in an environment extension (partly done);
• hook the commandStart linter into the git diff mechanism, so it only inspects code that changes, since the other is already compliant.

[Damiano Testa]

Since I imagine that this will noticeably reduce the running time of the linter, I was not too worried about its performance.

[Ruben Van de Velde]

In my experience such relative checks have a high likelihood of missing things over time and then failing when you touch code nearby. I'd carefully consider whether the tradeoffs are worth the increased complexity

[Damiano Testa]

That is a possibility, so I was also toying with the idea that maybe bors would run the linter on all of mathlib. At the same time, it is not like a misplaced whitespace is such a tragedy and there could be a monthly clean up run of all mathlib.

[Damiano Testa]

By the way, most style linters could hook into the "relative" mechanism as well. And, moreover, the "relative" mechanism need not be so fine-grained at the declaration (or even syntax node level): the linter could simply run on every modified file, not just on the modified parts of the files.

[Jovan Gerbscheid]

Michael Rothgang said:

I tried doing so in #26240

The result shows that this is indeed somewhat of a performance improvement, but it only saves about 5 seconds.

So, I think this does show that we might be better off with a "relative" linter, which runs on all changed files, and also runs every now and then on the whole of mathlib.

[Kenny Lau]

@Damiano Testa as a middle ground, is it possible to only do the linter for the files affected? (so bypassing the vulnerability of only focusing on the git diff, but also not running the linter on the whole mathlib)

[Jovan Gerbscheid]

I think that's what Damiano suggested in his last message

[Damiano Testa]

A first implementation of the "git-aware" version of the linter is available at #26299.

[Damiano Testa]

#26298 is a test PR that should show that the linter is active on modified files, new or otherwise.

EDIT: the test passed, since CI failed with error

Some required builds logged failures:
- Mathlib.Data.Array.Extract
- Mathlib.New

[Kenny Lau]

Bug report? Type (u+1) got corrected to Type (u + 1)

[Damiano Testa]

I've been using u + 1 when the linter suggested it. Though we can switch back in case that is not desired.

[Aaron Liu]

Kenny Lau said:

Bug report? Type (u+1) got corrected to Type (u + 1)

Is that not normal?

[Mario Carneiro]

that one might be worth taking a census for

[Mario Carneiro]

my guess is that humans usually write it without spaces, but the formatter always uses spaces there

[Mario Carneiro]

331 results for u + 1 and 94 for u+1 so maybe not

[Kenny Lau]

universe u

structure Foo : Type u :=
  (x : Type u)

/-
invalid universe level for field 'x', has type
  Type u
at universe level
  u+2
which is not less than or equal to the structure's resulting universe level
  u+1
-/

[Kenny Lau]

the printer sometimes uses u+1 and sometimes uses u + 1

[Mario Carneiro]

ah right, there is a second printer specifically for printing levels (src#Lean.Level.format)

[Mario Carneiro]

I think that one will also do things like (max u v)+1 instead of max u v + 1

[Mario Carneiro]

universe u v

/--
error: invalid universe level for field 'x', has type
  Sort (imax u v)
at universe level
  (imax u v)+1
which is not less than or equal to the structure's resulting universe level
  u+1
-/
#guard_msgs in structure Foo : Type u where x : Sort imax u v

/-- info: Type (imax u v) : Type ((imax u v) + 1) -/
#guard_msgs in #check Type imax u v

[Mario Carneiro]

I guess the normal printer also puts unnecessary parentheses there

[Edward van de Meent]

i've always treated universe expressions as though they were any others, meaning spaces around +... TIL some people disagree

[Jovan Gerbscheid]

Here's an interesting issue I encountered when leaving an extra space at the end of the @[simp] line:

@[simp]
theorem foo : 2 = 2 := rfl

It gives the error

remove line break in the source

This part of the code
  '@[simp]
theorem'
should be written as
  '@[simp]
theorem'


Note: This linter can be disabled with `set_option linter.style.commandStart false`

Both the replacement suggestion and the error message are confusing here.
Instead of just remove line break in the source, maybe a better message would be whitespace linter: please remove the extra whitespace.

[Damiano Testa]

This looks similar to #mathlib4 > Bug in commandStart linter error message @ 💬, right?

[Damiano Testa]

It is true that removing the line break would also silence the linter. I may make the message say that one way of silencing the linter is to follow its suggestion, but it is not the only way to silence it.

[Damiano Testa]

(Also, I have an option that automatically removes trailing whitespace on every line upon saving, so I am very rarely in a situation such as the one that you describe.)

[Jovan Gerbscheid]

I also have that option, but I'm not always saving files immediately :)

[Damiano Testa]

I do save pretty obsessively my files, to be honest... :slight_smile:

[Jovan Gerbscheid]

Oh, I only realize now that the linter meant to suggest

should be written as
  '@[simp] theorem'

[Damiano Testa]

Indeed, line breaks in the pretty-printer are not ideal, though...

[Damiano Testa]

But I am very pleasantly surprised by the fact that spaces are surprisingly good!

[Damiano Testa]

(And, besides, controllable by the user, at least if you can modify the code where the syntax is defined.)

[Damiano Testa]

Maybe I should also make it clear that, right now, I am aiming for the following goals from the commandStart linter:

• that it is active on most of mathlib;
• that it virtually never suggests something undesirable;
• that it is pretty consistent.

Being completely thorough is not (yet) a goal.

[Jovan Gerbscheid]

Do you think the linter should (after that goal is reached) enforce either a newline or not a newline in @[simp]? For long tags, they should definitely be on a separate line, but maybe we can tell it to remove the newline when the tag @[simp] is at most 10 (?) characters long.

[Damiano Testa]

I have not really thought about line breaks, but I would like it if it inspected the length of the string and, up to 100 chars, would suggest to place the whole command on a single line.

[Damiano Testa]

Breaking down more and more bits as the 100 chars limit is exceeded.

[Damiano Testa]

However, with line breaks and whitespace sensitivity, there are a lot of constraints and I have not really given it much thought.

[Damiano Testa]

For the moment, I find that allowing some (currently complete!) leeway in where the line-breaks are placed is actually a good compromise.

[Damiano Testa]

Btw, the "breaking down depending on the length" is also what the add_deprecation script does: it tries to fit @[deprecated (since := "..."] alias xxx := yyy on as few lines as possible, with breaks allowed at the attribute, and after the :=.