Restrict longLine warning to exceeding characters

Stream: mathlib4

[Damiano Testa]

Prompted by the discussion at #general > error lens in lean4 @ 💬 I opened #30902.

[Damiano Testa]

The proposal is to make the warning for the longLine linter span only the characters starting from the 101st, instead of the whole line exceeding the limit.

[Damiano Testa]

Personally, I think that this might probably a good idea, but since it might also reduce the visibility of the warning, I imagine that there are opposing views, hence why I am opening this thread!

[Damiano Testa]

So, what do you think about this?

[Ruben Van de Velde]

I'd test if it was still visible if you were just failing the check, so 101 columns

[Damiano Testa]

The tests already check that, and they do. The squiggle is only on the final character in those cases.

[Damiano Testa]

An alternative could be to start the warning somewhere in-between, like at 70 or so.

[Michael Rothgang]

I like starting the warning a little earlier, at 70 chars sounds good to me.

[Michael Rothgang]

One could go very fancy and try to find a matching word boundary (or even matching parentheses, so in

something_long_for_60_chars argument_1 (another long argument that pushes over the 101 chars)

only the second argument, which starts between column 60 and 70, gets highlighted.

[Eric Wieser]

I think it makes most sense to start the warning where the code actually needs wrapping

[Eric Wieser]

Given the gutter icons and possibility of error lens, I don't think we should be worried about a squiggle under a single extra character being hard to spot

[Eric Wieser]

Lean is already full of more important squiggles under single characters