Lean freezes with `#count_heartbeats`

Stream: lean4

[Floris van Doorn]

Can someone (on any operating system) test the following steps:

1. Create a new file in Mathlib with the following contents, and wait for it to compile

import Mathlib

variable {K : Type*} [Field K] {x y z : K}

-- slowly type the following line below this comment
-- attribute [-instance] Subsingleton.to_noZeroDivisors


attribute [-instance] Module.Free.of_subsingleton'

#count_heartbeats in
#synth Lean.Grind.NoNatZeroDivisors K

2. Below the comment, slowly type attribute [-instance] Subsingleton.to_noZeroDivisors
3. Wait for 1+ minutes

In this case, my Lean file becomes unresponsive (the yellow bars never disappear), and will not respond until Restart File/Restart Server or something similar is triggered

(tested on both Windows and Debian)

(#count_heartbeats is a Mathlib command, but I'm not sure if it itself it the culprit or just exposes something in Core)

[Michael Rothgang]

I can reproduce (Debian bookworm, on mathlib master). Typed attribute [-instance] (the last word at normal typing speed), then deleted letters until attribute [-ins, and now Lean is freezing beautifully.

[Michael Rothgang]

Commenting out the #count_heartbeats makes the issue disappear on my end.

[Marcus Rossel]

I can also reproduce this (on macOS). Oddly though, if I type very slowly, it doesn't freeze:

No Freeze

It seems waiting for the suggestions to roll in at attribute [-ins avoids the freeze.