Local linter

Stream: general

[Frédéric Dupuis]

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]

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

[Mario Carneiro]

The style linter doesn't work from inside lean

[Mario Carneiro]

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

[Alex J. Best]

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

[Mario Carneiro]

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]

Thanks!