Weird memory leak in simp?

Stream: lean4

[Palalansoukî]

First, forgive me for not being able to give a compact example to replicate the problem, since I haven't identified the exact cause of the problem.

I am working on a project to formalize logic . I recently updated Lean to v4.20.0-rc2 and encountered a weired memory leaks. The central part of the problem is as follows:

example : ![(x : V), x] 0 = x := by
  simp only [Matrix.cons_val_zero] -- memory leaks!

Where x is some complex term.

See here for details. This file depends on hundreds of local files, so it is difficult to extract mwe. mwe reproduce the error probably due to the same problem:

import Mathlib.Data.Fin.VecNotation

def x : ℕ := 999999^(999999^(999999^999999))

def y : ℕ := 9^9^9^9^9^9^9^9^9^9^9^9^9^9^9^9

example : ![x, 1] 0 = x := by
  simp only [Matrix.cons_val_zero] -- memory leak?

example : ![y, 1] 0 = y := by
  simp only [Matrix.cons_val_zero] -- (kernel) deep recursion detected

It is also odd to get a (kernel) deep recursion detected error for a very simple proposition.

Perhaps this is a bug in simp tactic?
I think this was not the case in the previous version (v4.18.0-rc1). What information can I provide to fix this problem?

[Sebastian Ullrich]

Can you please make "memory leak" more precise?

[Yury G. Kudryashov]

E.g., what tools tell you that it's a memory leak, not some other bug?

[Palalansoukî]

I checked using gnome-system-monitor. (If left untreated, it will occupy memory and freeze the PC.)

[Palalansoukî]

Can you please make "memory leak" more precise?

The yellow line on the left does not disappear even after the proof is finished, and in the meantime it continues to occupy memory (until PC freezes ...).

[Sebastian Ullrich]

That's not (just) a memory leak, that's a runaway process! This should usually be caught by the heartbeat/rec depth limits but apparently that doesn't happen (fast enough) here. Not sure what more can be said without an MWE.

[Jz Pan]

An unrelated code but with similar phenomenon: #Is there code for X? > Separability degree? @ 💬 which causes Lean to run forever

[Palalansoukî]

I found a mwe that probably causes the same problem (see also the first message I edited).

import Mathlib.Data.Fin.VecNotation

example :
    let x : ℕ := 999999^(999999^(999999^999999))
    ![x, 1] 0 = x := by
  simp only [Matrix.cons_val_zero] -- memory leak/runaway process?

[Jz Pan]

999999^(999999^(999999^999999)) is too big to evaluate.

[Jz Pan]

Related: #general > Panic in rw: Nat.pow exponent is too big