Debugging simp loops

Stream: lean4

[Patrick Massot]

Is there anything one can do to debug a simp call that loops forever (or at least long enough to time out)? I tried using set_option trace.Meta.Tactic.simp.rewrite true in but this simply freezes the Lean server.

[Sebastian Ullrich]

Do you get a (helpful) trace if you lower the timeout?

[Patrick Massot]

I tried

    set_option maxHeartbeats 10 in
    set_option trace.Meta.Tactic.simp.rewrite true in
    simp (config := {zeta := false}) [hγ₁.t₀]

which changes nothing (still freeze VSCode). Is that what you mean?

[Sebastian Ullrich]

Yes. I don't know off the top of my mind what could go wrong there, certainly the tracing should do allocations, i.e. use heartbeats