Zulip Chat Archive

Stream: general

Topic: Local linter


view this post on Zulip Frédéric Dupuis (Dec 16 2020 at 14:15):

Is the local linter (i.e. the one we can run locally with #lint) not automatically updated to be the same as on github? I've been caught out several times now by the 100 char per line linter on github, because it doesn't run locally.

view this post on Zulip Alex J. Best (Dec 16 2020 at 14:16):

The 100 lines check is actually a python script, rather than a linter written in lean
https://github.com/leanprover-community/mathlib/blob/master/scripts/lint-copy-mod-doc.py

view this post on Zulip Mario Carneiro (Dec 16 2020 at 14:16):

The style linter doesn't work from inside lean

view this post on Zulip Mario Carneiro (Dec 16 2020 at 14:17):

I would assume there is a way to run it locally...?

view this post on Zulip Alex J. Best (Dec 16 2020 at 14:17):

Yeah the shell script https://github.com/leanprover-community/mathlib/blob/master/scripts/lint-copy-mod-doc.sh does so.

view this post on Zulip Mario Carneiro (Dec 16 2020 at 14:18):

As mentioned in the other thread, lean 3's support for understanding its own syntax is really poor, so we can't do anything like "nonterminal simp check" or "line length" or "indentation" linting from a lean metaprogram

view this post on Zulip Frédéric Dupuis (Dec 16 2020 at 14:23):

Thanks!


Last updated: May 11 2021 at 23:11 UTC