Line length linter

Stream: general

[Scott Morrison]

Could the line length linter please report which file it is upset about?

I'm getting unhelpful messages like:

Run ./scripts/lint-style.sh
+ touch scripts/style-exceptions.txt
+ find src archive -name '*.lean'
+ xargs ./scripts/lint-style.py
Error: ERR_LIN: Line has more than 100 characters
Error: Process completed with exit code 123.

at https://github.com/leanprover-community/mathlib/pull/6198/checks?check_run_id=1887675372
(In this case I didn't touch too many files, so it can't be so hard to track down manually, but it would be nice to know.)

[Yakov Pechersky]

The annotation now appears in the Files changed page tab

[Yakov Pechersky]

At the location of the offending line

[Scott Morrison]

Nice!

[Eric Wieser]

We could of course fix it to make sure the information is reported everywhere

[Eric Wieser]

This page also shows the line number: https://github.com/leanprover-community/mathlib/actions/runs/561192202

It's just the log view which github decided to hide it from