Zulip Chat Archive

Stream: general

Topic: Debuging `simp` set


view this post on Zulip Yury G. Kudryashov (Apr 06 2020 at 01:01):

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?

view this post on Zulip Bryan Gin-ge Chen (Apr 06 2020 at 01:26):

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

view this post on Zulip Bryan Gin-ge Chen (Apr 06 2020 at 01:26):

The default is apparently 10000000.

view this post on Zulip Yury G. Kudryashov (Apr 06 2020 at 01:26):

Thank you, I'll try

view this post on Zulip Gabriel Ebner (Apr 06 2020 at 08:33):

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.


Last updated: May 08 2021 at 05:14 UTC