simpa?

Stream: general

[Yaël Dillies]

Could simpa? return the list of lemmas it used even when it fails/times out? It's really hard to debug a simpa call because Lean keeps that information away from me.

[Yaël Dillies]

Relatedly, simp should be able to tell me when there's a rewriting loop in my lemmas, since then two or three lemmas get used many many times. Could it do that and save me yet some time?

[Yaël Dillies]

Also is there an issue for the fact that simp [<- foo] does not forbid simp from rewriting with foo, hence almost certainly loops, rendering the <- mostly useless?

[Mario Carneiro]

You can use set_option trace.Meta.Tactic.simp.rewrite true to see information on what simp is doing even if it times out (although I think this isn't always the case depending on exactly how it fails). You can also try running it on the console, since then trace messages go directly to the terminal and the server doesn't have an opportunity to claw it back once it runs out of memory or whatever

[Kim Morrison]

We're working on better output when simp fails.