Can I run `lake exe runLinter` on a single file?

Stream: new members

[Fernando Chu]

I'm not sure where this command is defined, so I'm not sure what's the right thing to feed it. If not, is the only way of debugging the error below given by building all mathlib and then running the linter?

/- The `simpNF` linter reports:
SOME SIMP LEMMAS ARE NOT IN SIMP-NORMAL FORM.
see note [simp-normal form] for tips how to debug this.
https://leanprover-community.github.io/mathlib_docs/notes.html#simp-normal%20form -/
-- Mathlib.Combinatorics.SimpleGraph.Finite
Error: /home/lean/actions-runner/_work/mathlib4/mathlib4/pr-branch/Mathlib/Combinatorics/SimpleGraph/Finite.lean:111:1: error: @SimpleGraph.edgeSet_univ_card LINTER FAILED:
simplify fails on left-hand side:
failed to synthesize
  Nonempty ↑G.edgeSet
(deterministic) timeout at `typeclass`, maximum number of heartbeats (20000) has been reached

[Robin Arnez]

Putting #lint at the end of the file should do the trick

[Fernando Chu]

Thanks! However #lint succeeds locally, so is this just some weird CI business? What should I do?

[Damiano Testa]

The simp-normal form linter uses the whole environment. If you put #lint at the end of the file, the whole environment is what has been built up to that file. In CI, the whole environment also uses declarations that happen in later files and the check can fail later, but not fail on the file itself.

[Fernando Chu]

I see, thanks! So that means I have to rebuild all of mathlib to debug this, that's a bit sad :'(

[Robin Arnez]

If you're lucky, you might have cache

[Damiano Testa]

Looking at the failure, it seems like it is not an actual simp-NF exception, but rather that some change in the typeclass system causes a timeout and hence the simp-NF linter complains.

[Damiano Testa]

Did you add some instances?

[Damiano Testa]

The stated lemma does not seem to require any Nonemptyness...

[Fernando Chu]

I had changed some instances yes, and by trial and error I figured out the offending ones. These shouldn't have been instances and should have been defs anyways so it's fine. Thanks!