ERR_LIN

Stream: general

[Yaël Dillies]

Could the style linter tell us where the long lines are? The only way I know to check for them is by going in the "Files changed" tab on a PR, which isn't very practical, at least to me on big PRs.

[Yury G. Kudryashov]

I use something like git diff master | grep '.{102}' (actually, I use Emacs magit to get the diff and search for a regexp in this diff).

[Yaël Dillies]

Ooh, that's smart!

[Eric Wieser]

I broke this in #5952, it should be straightforward to extend the messages to include the missing information

[Eric Wieser]

Github is sort of at fault here; we're providing it the line number and filename in the message, but it's parsing them out then discarding them!

[Kevin Buzzard]

For some reason the linter itself cannot do this? It doesn't have access to the information?

[Kevin Buzzard]

I found this painful when I refactored all the _is_group_hom stuff

[Eric Wieser]

Are you talking about the lean linter or the style linter Kevin?

[Eric Wieser]

The problem with the style linter is that it currently prints out

::error file=X,line=Y,code=Z::Some information

and github says "Oh I know, you wanted to see 'Some information' and none of that silly colon stuff"

[Eric Wieser]

The fix is to just put X and Y inside Some information