distinguishing reasons for `nolint simpNF`?

Stream: mathlib4

[Kim Morrison]

We currently have many nolint simpNF in Mathlib. Sometimes these are because the simpNF linter is wrong, and we really want this simp lemma. Sometime they are because the simpNF linter crashes, and we just disable it to keep going.

Could someone come up with a mechanism to distinguish these? Either new syntax, or even just a standard comment?

At present nolint simpNF is not really actionable, because it's hard to tell whether one should be thinking about simp normal forms, or thinking about why the crash is occurring.

[Mario Carneiro]

I had no idea there were crashes being suppressed. Do you have more information about this?

[Kim Morrison]

Oh --- most of the nolint simpNFs in the library at this point are because the simpNF linter times out in typeclass search.

[Kim Morrison]

And I've just added about 10 (maybe more?) on nightly-testing.

[Yaël Dillies]

I'm not sure I agree with your original diagnosis. All the nolint simpNF I've added come with the comment -- eligible for dsimp.

[Kim Morrison]

What fraction of the nolint simpNF have such a comment?

[Yaël Dillies]

Not a computer, so can't check, but something like 70% in the files I work on (basic algebra files)

[Kim Morrison]

A quick random sample provides messages:

-- These lemmas have always been bad (#7657), but leanprover/lean4#2644 made `simp` start noticing

-- This lemma has always been bad, but leanprover/lean4#2644 made `simp` start noticing

-- Porting note (#10675): dsimp can not prove this

-- Porting note: `simpNF` should not trigger on `rfl` lemmas.
-- see https://github.com/leanprover/std4/issues/86

<no comment>