Stream: new members
Topic: simp_nf linter
Frédéric Dupuis (Oct 30 2020 at 12:57):
Is it possible to run the
simp_nf linter on one particular file (including everything it imports) without running the full lint mathlib script? I'm currently getting errors in a PR (namely #4824) where the changes I made in one file caused several lemmas in another file it imports to become provable by simp, and
#lint at the end of the file doesn't catch them.
Floris van Doorn (Oct 30 2020 at 18:49):
#lint does run the
lint_nf linter in the file where you type it. However, when adding more imports to a file, the
lint_nf linter might raise more errors, if the imported files contain conflicting simp lemmas. That's why the mathlib script might raise an error you didn't find.
You can also run
#lint_mathlib in any file to lint all files of mathlib that you've imported.
Frédéric Dupuis (Oct 30 2020 at 18:51):
#lint_mathlib is exactly what I was looking for.
Kevin Lacker (Oct 30 2020 at 19:09):
is the full lint mathlib script, ie
lean --run scripts/lint_mathlib.lean, just supposed to take a large amount of time? it does for me
Bryan Gin-ge Chen (Oct 30 2020 at 19:10):
I think so. It takes our CI 55 minutes or so.
Floris van Doorn (Oct 30 2020 at 19:14):
Yes. Some of the linters are quite slow, and they are called on all declarations in mathlib.
Last updated: May 14 2021 at 23:14 UTC