simp_nf linter

Stream: new members

[Frédéric Dupuis]

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]

#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]

Thanks! #lint_mathlib is exactly what I was looking for.

[Kevin Lacker]

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]

I think so. It takes our CI 55 minutes or so.

[Floris van Doorn]

Yes. Some of the linters are quite slow, and they are called on all declarations in mathlib.