lake exe lint-style --update

Stream: general

[Sébastien Gouëzel]

In a PR where the line count of a file goes above the limit, the style linter check tells me

error: Mathlib/MeasureTheory/Measure/Typeclasses.lean:1: file contains 1531 lines, try to split it up
error: found 1 new style error(s)
run `lake exe lint-style --update` to ignore all of them

So I ran the command lake exe lint-style --update, but it failed with an error

error: Mathlib\Algebra\BigOperators\Group\Finset.lean:1: file contains 2254 lines, try to split it up
...
error: Mathlib\Topology\UniformSpace\Basic.lean:1: file contains 1768 lines, try to split it up
uncaught exception: unspecified system_category error (error code: 193)

I'm on windows. Does it ring a bell?

[Damiano Testa]

The initial / became \, weird.

[Sébastien Gouëzel]

(and it emptied the file scripts/style-exceptions.txt)

[Damiano Testa]

Also, is the initial error correct, as in the file Mathlib/MeasureTheory/Measure/Typeclasses.lean really has 1531 lines?

[Sébastien Gouëzel]

Yes, the error is genuine, it's only the fixing step which is buggy.

[Damiano Testa]

From the change in slashes, I wonder whether there is a misparsing of path separators.

[Damiano Testa]

(Btw, I hope that many of these issues will disappear if the longFile syntax linter will get merged, as there exceptions will be in-place and there will no longer be the need of a separate exception file.)

[Damiano Testa]

I am not sure, but I think that what happened is that the linter found your error, correctly identifying \ as path separators. However, when it then tried to "update" stuff, it used the incorrect path separator, found no files with the new paths and cleared the exceptions. Finally, it realized that there were style exceptions, even though the newly cleared exceptions file told it that there were none.

[Damiano Testa]

Or something along these lines.

[Damiano Testa]

(Sorry, I have to leave now and I am not too familiar with the TextBased code anyway. I'll ping @Michael Rothgang, in case he has not noticed this! :smile: )

[Michael Rothgang]

Thanks for pinging me. I also wonder if path separators are an issue. (I remember looking into this for mk_all, but perhaps I did not check if lint-style was also affected.) I will try to investigate tomorrow, but no promises (weekend and such).

[Michael Rothgang]

In the mean-time, you can certainly add the exception manually, or I can update the file for you.

[Michael Rothgang]

Sorry for the delay. I found a moment to investigate now:

• with #15610 landed, the text-based linter for long files is basically unused (in fact, #16299 proposes removing it). All remaining text-based linters should usually be fixed (not allowed); hence, this particular issue should not appear in practice any more.
• The text-based linter was indeed not taking different path separators into account. #16329 should fix this. @Sébastien Gouëzel Do you have a chance to test this change?
  (It is fine if not; the PR seems like a strict improvement anyway.)