Lots of crashes after updating to `leanprover/lean4:v4.6.0`

Stream: lean4

[Geoffrey Irving]

I'm getting a lot of stack overflows after updating to v4.6.0. This is in slightly fragile code that has constants like 2^64 everywhere, and each crash is fixable by replacing simp uses with rw, so presumably what's happening is that simp is now digging into the constants somehow in ways it didn't use to. It's slightly annoying to minimize as it takes down the whole Lean server each time:

Lean server printed an error: libc++abi: terminating due to uncaught exception of type lean::stack_space_exception: deep recursion was detected at 'replace' (potential solution: increase stack space in your system)

If this seems worth minimizing I can do that.

[Matthew Ballard]

Wild guess: some new simprocs might be the culprit. I assume these can be disabled?

[Jannis Limperg]

set_option simprocs false

[Geoffrey Irving]

Here's a small example:

import Mathlib.Data.UInt

lemma UInt64.toNat_add (m n : UInt64) : (m + n).toNat = (m.toNat + n.toNat) % UInt64.size := by
  simp only [UInt64.toNat, UInt64.add_def]
  simp only [HAdd.hAdd, Add.add, Fin.add, Nat.add_eq]

[Geoffrey Irving]

That set_option doesn't seem to fix it.

[Geoffrey Irving]

Here's a version that doesn't crash, using different simp lemmas:

import Mathlib.Data.UInt

lemma UInt64.toNat_add (m n : UInt64) : (m + n).toNat = (m.toNat + n.toNat) % UInt64.size := by
  simp only [UInt64.toNat, UInt64.add_def, Fin.add_def]

[Patrick Massot]

@Geoffrey Irving I suspect Leo will be very interested, but only if you build a Mathlib-free example.

[Geoffrey Irving]

Here's a crash with no imports:

theorem UInt64.add_def (a b : UInt64) : a + b = ⟨a.val + b.val⟩ := rfl

theorem UInt64.toNat_add (m n : UInt64) : (m + n).toNat = (m.toNat + n.toNat) % UInt64.size := by
  simp only [UInt64.toNat, UInt64.add_def]
  simp only [HAdd.hAdd, Add.add, Fin.add, Nat.add_eq]

[Patrick Massot]

Great, you can now open an issue in the lean4 repo.

[Geoffrey Irving]

https://github.com/leanprover/lean4/issues/3267