Questions about grind

Stream: CSLib

[Ching-Tsun Chou]

I find grind rather hard to understand. I moved the following code:

@[scoped grind =]
def mtr (DA : DA State Symbol) (s : State) (xs : List Symbol) := xs.foldl DA.tr s

@[simp, scoped grind =]
theorem mtr_nil_eq {DA : DA State Symbol} {s : State} : DA.mtr s [] = s := rfl

from DFA.lean to DA.lean, because I want to use them in general constructions (such as product) about DA, not just about DFA (which extends DA). This move breaks quite a few grinds in various proofs about DFA and I had to give [DA.mtr] explicitly to those grinds to fix them. Why?

More generally, how should one proceed when grind fails? I find its error messages rather mysterious.

[Chris Henson]

Based on your description, my guess would be that you are just missing an open scoped DA after changing what namespaces these are in.

[Ching-Tsun Chou]

You are right! Thanks!

[Pieter Cuijpers]

I get a CI error on cslib#220 saying:
error: CslibTests/GrindLint.lean:74:0: ❌️ Docstring on #guard_msgs does not match generated message:

I admit, I've been guessing my way around in the use of @[grind]. Would appreciate some help on understanding what is going wrong.

[Chris Henson]

There is test in the mentioned file that checks for grind annotations that trigger a high number of instantiations. The solution here is to either remove the annotations or use the constraint feature to limit them. (You'll also see some exceptions in that test, but we're trying not to add to this)