Too many lines linter

Stream: PR reviews

[Kim Morrison]

Could someone assist me with the failure of the too-many-lines linter at #15397:

::ERR file=Mathlib/SetTheory/Cardinal/Ordinal.lean,line=1,code=ERR_NUM_LIN::
Mathlib/SetTheory/Cardinal/Ordinal.lean:1 ERR_NUM_LIN: file contains 1501 lines (at most 1700 allowed), try to split it up

Possible ways to help:

• work out what has gone wrong here and fix it: 1501 < 1700
• modify the error message so it gives actionable advice including how to add this file to the exceptions
• tell me where the exceptions live! Make the exceptions more robust so merely changing the number of lines doesn't require changing the exception
• add an exception to this PR

[Damiano Testa]

I have not read carefully the relevant linter, but the doc-string for this error message says the following:

  /-- The current file was too large: this error contains the current number of lines
  as well as a size limit (slightly larger). On future runs, this linter will allow this file
  to grow up to this limit. -/

[Damiano Testa]

It suggests that a second run would not make the linter complain, but I do not understand how that mechanism can work.

[Damiano Testa]

It does explain why a larger limit than what it says make the linter unhappy...

[Damiano Testa]

I'll ping @Michael Rothgang, since I think that he will know what to do!

[Kim Morrison]

Presumably I need to run something and commit something in order for it to behave differently next time!

[Damiano Testa]

Yes, I think that Michael had a "shake linters" command, but I do not know the status of that.

[Damiano Testa]

I also know that Yaël was not too happy with the linter suggesting to split the file by default, since, unless you know what you are doing, you should add an exception, rather than splitting the file!

[Ruben Van de Velde]

Ugh, someone rewrote that linter in lean. I added an exception blindly

[Michael Rothgang]

Damiano Testa said:

Yes, I think that Michael had a "shake linters" command, but I do not know the status of that.

Side aspects first: yup, I rewrote that lint in Lean, you're welcome.
#14697 rewrites the automatic updating of style exceptions in Lean: once that PR is merged, you can just say lake exe lint_style --update to ignore the exception (and the CI error should tell you so). Would somebody (Damiano maybe) like to review it? I just merged master again.

[Michael Rothgang]

Now for the main error message: I think I understood what happened.
TL;DR: adding an exception is the correct call in the short term.

[Michael Rothgang]

Long version:

1. The file SetTheory/Ordinal had less than 1500 lines prior to the PR, so passed the linter. After the PR, it had 1501 lines, which exceeds the cut-off of 1500 lines. Yes, this means small perturbations can cause a sudden error. I don't see how to fully avoid this.
   (Once a file is too large, the linter adds some slack to avoid flagging every PR adding just a hand-ful of lines. I could, as a one-time change, add such entries for every file with currently 1300 lines. Let me know if this would help.)

2. Because of this, the linter complained (like it should). The error message has a bug, though: it should not mention 1700 (as there is no exception for this file yet). Let me send a PR...

3. The PR above will add actionable advice on updating this. If reviewing this takes too long, I can add something in the short term (only to remove it again in #14697).
4. As for silencing the linter: in the short term, adding an exception seems the right call. If you see an obvious way to split a few hundred lines off that file, that's obviously also fine --- but definitely optional!

[Ruben Van de Velde]

Does the lean translation have a command to update the exceptions automatically?

[Michael Rothgang]

For now, update-style-exceptions still handles this.

[Michael Rothgang]

After #14697, this is replaced by lake exe lint_style --update

[Michael Rothgang]

#15414 fixes the error message; review welcome!

[Kim Morrison]

Thank you, Michael, for rewriting the linter in Lean, to begin with. I think this really helps for maintainability, plus its great when we learn about missing features or problems in Lean itself from doing this.

[Michael Rothgang]

Thanks a lot for the reviews! I merged master on #14697, can somebody re-bors it?

[Damiano Testa]

I was thinking that maybe the "too many lines" linter could be implemented as a syntax linter that emits a warning when the current declaration has starting position above 1500. The mechanism to silence it would be to make its option be a natural number and the linter actually compares to 1500 the difference of the current position of the command and the value of the option.

[Damiano Testa]

So, for instance, writing set_option linter.longFile 2000 at the beginning of a file (or, really anywhere before the line 1500), allows the file to be up to 3500 lines long, before the linter starts complaining.

[Damiano Testa]

This would make it very easy to silence the linter, would not require a list of exceptions, other than the per-file set_options.

[Damiano Testa]

Does this seem like an improvement over the current situation?

[Damiano Testa]

Since it was completely straightforward to implement, I just PRed this syntax linter! #15610

I will wait for CI to tell me which files do not comply with the linter.

[Damiano Testa]

An advantage of the syntax linter is that it can also self-correct: when it reaches the last line of a file, the linter can make sure that the option for the linter is not exceedingly large. Currently, the long file linter seems to operate with increases of 200.

[Kevin Buzzard]

Wouldn't it be less confusing to have the number being the bound, rather than bound-1500?

[Damiano Testa]

Yes, indeed, this is what the implementation does actually.

[Damiano Testa]

And another advantage is that now you write the exception directly on the file, rather than having to update a separate file with all the exceptions.

[Michael Rothgang]

Thank you for porting my Lean port of the python linter into a proper syntax linter. I'll be happy to review it next week (if nobody else has done so by then).