command to lint a single declaration?

Stream: general

[Scott Morrison]

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]

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

[Scott Morrison]

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]

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]

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]

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]

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]

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

[Scott Morrison]

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

[Scott Morrison]

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