Topic: Local linter
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.
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
Mario Carneiro (Dec 16 2020 at 14:16):
The style linter doesn't work from inside lean
Mario Carneiro (Dec 16 2020 at 14:17):
I would assume there is a way to run it locally...?
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.
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
Frédéric Dupuis (Dec 16 2020 at 14:23):
Last updated: Aug 03 2023 at 10:10 UTC