Trace simp

Stream: mathlib4

[Yury G. Kudryashov]

Is there an option to ask simp to print used lemmas when it applies them? I need to debug a cycle that results in "deep recursion" error.

[Alex J. Best]

There is an option with simp and rewrites in the name that I usually use tab completion to find the precise name of maybe Trace.Meta.Simp.rewrites but I'm not sure

[Yury G. Kudryashov]

Indeed,

set_option trace.Meta.Tactic.simp.rewrite true

works. Thanks!

[Oliver Nash]

Do we have (or could we create) a place (maybe on the website) to store especially-useful set_option commands like this?

[Alex J. Best]

Maybe we can put them on the tips and tricks page? https://leanprover-community.github.io/tips_and_tricks.html which really needs refreshing for lean 4 by now anyway