idle thought on 100 char line linter

Stream: mathlib4

[Kevin Buzzard]

I'm doing the chore of reviewing #20595, and 99% of the changes are things like replacing [LinearOrderedField 𝕜] with [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]. The new spelling is many more characters than the old one. Sometimes this does not cause an overflow, such as here (screenshot from github):

Screenshot from 2025-04-06 22-12-23.png

However often these changes tip lines above 100 characters, giving us diffs like this:

Screenshot from 2025-04-06 22-14-04.png

Notice the difference? This second diff is much harder to check visually, because the changes are not highlighted.

It occurred to me that for huge chore PRs like this it would be really nice to be able to temporarily switch off the 100 line linter and see the diff displayed on github with the highlights but with many lines more than 100 chars long, and then to press another button and magically everything gets repaginated. Is this too much of a long shot and/or niche request? I have personally several times been caught out by people making suggestions on github which I've committed and then the next day looked at my PR and it's failing CI because a line is > 100 chars. Instead of complaining is it possible to just repaginate just before merging? Or even better allow lines of more than 100 chars and just have some bot come along daily and fix them up? Are there unacceptable risks to this idea?

[Edward van de Meent]

Having a bot add commits to the remote version of a branch can cause merge conflicts when done too early.

[Edward van de Meent]

This isn't exactly an unacceptable risk, but still worth avoiding if there's a better solution

[Vlad Tsyrklevich]

If there was an auto-formatter to do the line breaks, one easy way to fix the problem of reviewing difficulty is to have the first commit be just the text replacement, and the second (or last) commit be the auto-formatting, so that reviewers can just look at the first commit.

[Sabbir Rahman]

I really miss an auto-formatter for lean4, in my day job in software engineering, we have to mandatorily use auto formatting to keep styles consistent and make pr reviewing easy

[Jz Pan]

Or ask github to highlight changes in a multiline diff.

[Patrick Massot]

Sabbir, everybody here knows this. It will come at some point, but it’s a lot of work due to the immense flexibility of the Lean 4 syntax.