Zulip Chat Archive

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 (Nov 09 2023 at 21:37):

lake exe runMathlibLinter

David Renshaw (Nov 09 2023 at 21:38):

you can run it on individual files

lake exe runMathlibLinter  Mathlib.Algebra.Order.SMul

Newell Jensen (Nov 09 2023 at 21:39):

David Renshaw said:

you can run it on individual files
lake exe runMathlibLinter  Mathlib.Algebra.Order.SMul

Perfect thanks!

Newell Jensen (Nov 09 2023 at 21:42):

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

Alex J. Best (Nov 09 2023 at 23:05):

Which error?

Newell Jensen (Nov 09 2023 at 23:33):

Alex J. Best said:

Which error?

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

Alex J. Best (Nov 10 2023 at 00:24):

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

Newell Jensen (Nov 10 2023 at 21:11):

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

Last updated: Dec 20 2023 at 11:08 UTC

leanprover-community / mathlib