Debuging `simp` set

Stream: general

[Yury G. Kudryashov]

I'm formalizing quaternions, and I have a timeout in simp probably because of some cycle in my simp set. Can I ask Lean to simp for some fixed amount of cycles, then report lemmas it used?

[Bryan Gin-ge Chen]

Maybe supplying max_steps with simp {max_steps:= 100} will help?

[Bryan Gin-ge Chen]

The default is apparently 10000000.

[Yury G. Kudryashov]

Thank you, I'll try

[Gabriel Ebner]

The standard way is to enable set_option trace.simplify.rewrite true, this outputs one line per used simp lemma. You can then use try_for 12345 { simp } to stop simp before it is finished.