diagnosing loops in `simp`

Stream: general

[Scott Morrison]

Can someone remind me what I'm meant to do to diagnose simp apparently going into an endless loop, and ending in a timeout? There must be some option to set so I can see which lemmas it is attempting to apply.

[Scott Morrison]

Ah, okay: set_option trace.simp_lemmas true. Curiously in VSCode set option trace.simp doesn't include in its autocomplete suggestions trace.simp_lemmas.

[Scott Morrison]

Oh, and it's trace.simplify that I want anyway.

[Kevin Buzzard]

Scott -- if this is not mentioned in the simp docs then add one para and make a PR.

[Kevin Buzzard]

Or just download

[Kevin Buzzard]

https://github.com/leanprover/mathlib/blob/master/docs/extras/simp.md

[Kevin Buzzard]

and edit it and email it me.

[Kevin Buzzard]

Let's get these answers down in a canonical place.