Detecting which lemmas make simp loop

Stream: lean4

[Yaël Dillies]

Could simp tell me upfront what lemmas it is looping with when it loops? There's usually only two or three lemmas involved, so it should be easy to figure out which ones they are just by counting the number of times each lemma is used, or maybe by figuring out the pattern in the rewrites.

[Yaël Dillies]

Eg in

def foo : Nat := 0
def bar : Nat := 0

@[simp] theorem foo_eq_bar : foo = bar := rfl
@[simp] theorem bar_eq_foo : bar = foo := rfl

example : foo = bar + 1 := by simp

I get the error

tactic 'simp' failed, nested error:
maximum recursion depth has been reached
use `set_option maxRecDepth <num>` to increase limit
use `set_option diagnostics true` to get diagnostic information

[Yaël Dillies]

If I add set_option diagnostics true (where is trace.simplifier.rewrite gone btw? I don't seem to be able to know what the rewrites actually were), then it tells me (after some clicking around)

[simp] used theorems (max: 252, num: 2): ▶
[simp] tried theorems (max: 252, num: 2): ▼
  foo_eq_bar ↦ 252, succeeded: 252
  bar_eq_foo ↦ 251, succeeded: 251
use `set_option diagnostics.threshold <num>` to control threshold for reporting counters

[Yaël Dillies]

Great! Could the simp error tell me upfront that foo_eq_bar and bar_eq_foo were the problematic lemmas?

[Mauricio Collares]

Yaël Dillies said:

(where is trace.simplifier.rewrite gone btw? I don't seem to be able to know what the rewrites actually were)

trace.Meta.Tactic.simp.rewrite

[Yaël Dillies]

In real life, there's not just one simp call which I can isolate for a set_option diagnostics true/set_option trace.Meta.Tactic.simp.rewrite true analysis, but rather many simp calls with many handspecified lemmas, and if the root cause can be automatically figured out why should I have to quit my workflow and get into debugging mode?

[Sebastian Ullrich]

I think the simplest solution here would be to auto-attach the diagnostics output when running into the depth limit

[Yaël Dillies]

Sure, but the diagnostics still require some clicking around and don't actually explain what happened. Like sure I can understand what they mean, but a beginner probably won't (and I don't think we should expect them to?). Can't we slightly post-process the output?

[Yaël Dillies]

Yaël Dillies said:

the diagnostics still require some clicking around

Btw why is it so slow to click around diagnostics? It takes 5-10 seconds for the collapsed list to expand when I click it

[Kevin Buzzard]

Is it huge? I've seen uncollapsing lists crash VS Code when typeclass inference goes haywire, because they can be revealing literally hundreds of thousands of lines.

[Yaël Dillies]

No, it's literally this:
Yaël Dillies said:

[simp] used theorems (max: 252, num: 2): ▶
[simp] tried theorems (max: 252, num: 2): ▼
  foo_eq_bar ↦ 252, succeeded: 252
  bar_eq_foo ↦ 251, succeeded: 251
use `set_option diagnostics.threshold <num>` to control threshold for reporting counters

[Sebastian Ullrich]

Cannot reproduce on Lean master, it's instantaneous

[Yaël Dillies]

Interesting... will have to try again