stack overflow in linarith

Stream: mathlib4

[Heather Macbeth]

Can anyone reproduce a stack overflow in linarith on the following code?

import Mathlib.Tactic.Linarith

example (p T m l : ℕ) (hp : 2 ≤ p) (hTp : p < T ^ 2)
    (hm1 : 1 < m) (hmp: m < p) (hmT : T ≤ m) (hl: p = m * l)
    (hl1 : 1 < l) :
    T * l ≤ m * l := by
  nlinarith

I get in the infoview

Server process for *** crashed, likely due to a stack overflow or a bug.

and pop-ups

Lean server printed an error: libc++abi.dylib: terminating with uncaught exception of type lean::heartbeat_exception: (deterministic) timeout

and

The Lean Server has stopped processing this file.

[Floris van Doorn]

For me Lean just tries to compile the example for many minutes, without finishing or crashing.

[Henrik Böving]

Note that this is not a stack overflow but a heartbeat timeout. Heartbeats are a concept for Lean 4 to track how much work it has done on some task and abort if it exceeds a certain limit so things dont hang up...I've never seen a heartbeat timeout from C++ though usually lean throws them on its own.

[Heather Macbeth]

I opened !4#2715 to track this issue.