run linters locally

Stream: mathlib4

[Newell Jensen]

Is there a way to run (all?) the linters locally? All I currently run locally is ./scripts/lint-style.py <filename> and wondering if there is something else I can run to better test against linting errors before pushing to github?

[David Renshaw]

lake exe runMathlibLinter

[David Renshaw]

you can run it on individual files

lake exe runMathlibLinter  Mathlib.Algebra.Order.SMul

[Newell Jensen]

David Renshaw said:

you can run it on individual files

lake exe runMathlibLinter  Mathlib.Algebra.Order.SMul

Perfect thanks!

[Newell Jensen]

Hmmm, this doesn't catch the linting error I get from the CI build.

[Alex J. Best]

Which error?

[Newell Jensen]

Alex J. Best said:

Which error?

https://github.com/leanprover-community/mathlib4/actions/runs/6817820957/job/18542139285?pr=8223

[Alex J. Best]

Hmm, that should definitely show up when the linter runs locally on that file, weird

[Newell Jensen]

Okay, the issue was I needed to run lake build before running the linter to get it to work properly.

[Jineon Baek]

I wish this info on how to run CI locally is included in how-to documents on contributing to mathlib4. Or does it? I never seen one until I searched this thread

[Michael Rothgang]

I agree it would be useful - and a PR adding it would be welcome!

[Michael Rothgang]

That said: right now, running all mathlib linters is kind of slow (10 minutes on CI, easily 20 on my computer): there is a linter about all lemmas marked with the @[simp] attribute having the right shape - and this linter is necessarily global, and takes a while.

[Michael Rothgang]

I never run these linters locally, but rely on CI to catch these. There is no expectation that you do so.

[Michael Rothgang]

Another option: you can put #lint at the end of your file, and it will tell you about all linters for the file you're editing. That's usually good enough!

[Michael Rothgang]

Let me also add: after a small change (which I intend to PR soon), you will be able to run lake lint filename instead, and can also select individual linters. No need to memorise runLinter.