Excessive grind?

Stream: CSLib

[Ching-Tsun Chou]

In PR cslib#216, I encounter in lake test the type of failures shown below. Any idea how I may fix them? More complete error messages are available in the PR.

info: CslibTests/GrindLint.lean:76:0: instantiating `Cslib.Automata.NA.Buchi.concat_language_eq` triggers more than 100 additional `grind` theorem instantiations
info: CslibTests/GrindLint.lean:76:0: Cslib.Automata.NA.Buchi.concat_language_eq
[thm] instances
  [thm] Set.mem_setOf_eq ↦ 12
  [thm] Cslib.Automata.Acceptor.mem_language ↦ 9
  [thm] Cslib.Automata.Acceptor.language.eq_1 ↦ 9
  [thm] Set.setOf_false ↦ 6
  [thm] Set.setOf_true ↦ 6
  [thm] Cslib.Automata.NA.FinAcc.toDAFinAcc_language_eq ↦ 5
  [thm] Cslib.Automata.NA.FinAcc.instAcceptor.eq_1 ↦ 5
  [thm] Cslib.FLTS.mtr_nil_eq ↦ 4
  [thm] Cslib.FLTS.mtr.eq_1 ↦ 4
  [thm] Cslib.Automata.DA.FinAcc.toNAFinAcc_language_eq ↦ 4
  [thm] Cslib.Automata.NA.toDA.eq_1 ↦ 4
  [thm] Cslib.Automata.DA.FinAcc.instAcceptor.eq_1 ↦ 4
  [thm] Cslib.Automata.DA.FinAcc.toNAFinAcc.eq_1 ↦ 4
  [thm] Cslib.Automata.NA.FinAcc.toDAFinAcc.eq_1 ↦ 4
  [thm] Cslib.LTS.toFLTS_mtr_setImageMultistep ↦ 3
  [thm] Cslib.FLTS.toLTS.eq_1 ↦ 3
  [thm] Cslib.LTS.toFLTS.eq_1 ↦ 3
  [thm] Cslib.Automata.DA.toNA.eq_1 ↦ 3
  [thm] Cslib.LTS.setImageMultistep_foldl_setImage ↦ 2
  [thm] Cslib.Automata.ωAcceptor.language.eq_1 ↦ 2
  [thm] Cslib.Automata.NA.Buchi.instωAcceptor.eq_1 ↦ 2
  [thm] Cslib.Automata.NA.Buchi.concat_language_eq ↦ 1
  [thm] Cslib.Automata.NA.concat.eq_1 ↦ 1

[Chris Henson]

With the bump to v4.27.0-rc1 we can now add constraints to grind_pattern that could help. I've not used it much yet, but see the docs added in lean4#11429.

[Ching-Tsun Chou]

I fixed the failures by removing the grind annotations from the offending theorems and passing them explicitly to grind when needed.

[Ching-Tsun Chou]

I did play with changing the patterns in the grind annotations of those theorems from = to others, but none worked.