Zulip Chat Archive

Stream: new members

Topic: simp_nf linter


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Frédéric Dupuis (Oct 30 2020 at 18:51):

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

view this post on Zulip 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

view this post on Zulip Bryan Gin-ge Chen (Oct 30 2020 at 19:10):

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

view this post on Zulip 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