convert tactic hangs

Stream: mathlib4

[Eric Wieser]

The following code results in a hang that maxHeartbeats seems unable to stop:

import Mathlib.Tactic.Convert

def Nat.choose : Nat → Nat → Nat
  | _, 0 => 1
  | 0, _ + 1 => 0
  | n + 1, k + 1 => choose n k + choose n (k + 1)

structure Foo (n : Nat)


set_option maxHeartbeats 200 -- be quick please

def foo (x : Foo (Nat.choose 2000 1500)) : Foo (Nat.choose 2000 500) := by
  convert x using 1 -- hangs forever

if you add and remove a space after the 1, then you get a new hanging lean background process each time

[Johan Commelin]

I guess this is a bug in convert, right? Or do you think it is lower-level than that?

[Jireh Loreaux]

isn't this exactly caused by lean4#5565 ?

[Johan Commelin]

Sounds likely, yes! @Eric Wieser do you agree this is probably the cause?

[Jireh Loreaux]

@Kim Morrison I think you asked if there was a reason to cut a bugfix release about lean4#5565. This might be it.

[Eric Wieser]

I think this might also be a lower level issue caused by using MVarId.assign, which would pass a huge Nat to the kernel where no further timeout checks are made

[Eric Wieser]

Jireh Loreaux said:

Kim Morrison I think you asked if there was a reason to cut a bugfix release about lean4#5565. This might be it.

Even if we don't do a 4.12.0 bug fix release, it would be good to get the lean4#5566 patch into a 4.13.0rc2

[Yaël Dillies]

You mean 4.13.0-rc3 ?

[Eric Wieser]

Nope, looks like I mean rc4

[Kyle Miller]

I don't think this is a convert issue, given that rfl hangs too:

def foo : Foo (Nat.choose 2000 1500) = Foo (Nat.choose 2000 500) := by
  rfl

[Eric Wieser]

Huh, I was sure I tried that when minimizing!

[Johan Commelin]

@Kyle Miller Is this a known issue? Or should we report it at core?

[Eric Wieser]

Maybe this message is relevant?

[Kyle Miller]

Seems like a good idea to report it. I don't immediately see any related issues.

[Johan Commelin]

Is this the same issue as https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.E2.9C.94.20.60rfl.60.20regression.3F ?

[Kyle Miller]

One difference is that this example never triggers a timeout, which on its own is worth figuring out. The other thread at least gets a "max recursion depth".

[Johan Commelin]

That's a good point