Zulip Chat Archive

Stream: general

Topic: Line length linter


view this post on Zulip Scott Morrison (Feb 12 2021 at 14:00):

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.)

view this post on Zulip Yakov Pechersky (Feb 12 2021 at 14:01):

The annotation now appears in the Files changed page tab

view this post on Zulip Yakov Pechersky (Feb 12 2021 at 14:01):

At the location of the offending line

view this post on Zulip Scott Morrison (Feb 12 2021 at 14:06):

Nice!

view this post on Zulip Eric Wieser (Feb 12 2021 at 14:22):

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

view this post on Zulip Eric Wieser (Feb 12 2021 at 14:23):

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


Last updated: May 10 2021 at 00:31 UTC