Zulip Chat Archive

Stream: general

Topic: command to lint a single declaration?

Scott Morrison (Nov 10 2022 at 10:56):

I'm getting timeouts in the simp_nf linter. Is there a command to run the simp_nf linter on a single declaration, or do I need to use the plumbing functions?

Anne Baanen (Nov 10 2022 at 11:21):

I usually put something together along the lines of run_cmd tactic.get_decl your_decl_name >>= linter.simp_nf.test`

Scott Morrison (Nov 10 2022 at 11:26):

And if I have a "non-local" simp_nf timeout (i.e. running the linter in the same file as the declaration succeeds, but fails during CI when the linter is running with the whole library imported), then I have to do this in all.lean, right?

Scott Morrison (Nov 10 2022 at 11:27):

Seems a real headache to test solutions. I guess if I can reproduce the failure at the bottom of all.lean I can try to find a minimal set of imports that display the problem, and then just test solutions recompiling that.

Scott Morrison (Nov 10 2022 at 11:28):

I'm off to sleep, but if anyone is excited about fighting the simp_nf linter, I'd love some help with these: https://github.com/leanprover-community/mathlib/actions/runs/3435238591/jobs/5727462915 from my last refactoring PR #17435.

Scott Morrison (Nov 10 2022 at 11:29):

I think I've dealt with the problems in order/hom/set.lean and data/nat/cast/with_top.lean, but all the others seem to be non-local.

Scott Morrison (Nov 10 2022 at 11:29):

I'm guessing some casting instances are firing in a different order than previously due to my import restructuring, but that's just a hunch.

Eric Wieser (Nov 10 2022 at 11:30):

I think there's a lint only command of some form

Scott Morrison (Nov 10 2022 at 11:30):

I think that just restricts the set of linters, not the set of declarations.

Scott Morrison (Nov 10 2022 at 11:31):

Anne's suggestion above works fine. It's just a hassle to have to do the testing in all.lean...

Last updated: Aug 03 2023 at 10:10 UTC