grind stamina

Stream: lean4

[Jakob von Raumer]

Is there any blanket option to give the modules of grind more time? We have a case in the RISC-V model where a grind proof seems to fail because some horrible nesting of conjunctions just seems too deep for grind (deleting a few of the clauses makes it work again)

[Robin Arnez]

The relevant details are in docs#Lean.Grind.Config. Maybe grind (splits := 10) or something would work?

[Jakob von Raumer]

Hm, then I need to investigate further. I already increased all of the config options

[Kim Morrison]

Jakob von Raumer said:

Hm, then I need to investigate further. I already increased all of the config options

The diagnostic output on failure tells you which limits were reached.