Repeat tactic does not terminate instead of giving an error or functioning as it should.

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
    • Specifically, check out the wishlist, open RFCs,
      or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

Repeat tactic does not terminate instead of giving an error or functioning as it should.

Steps to Reproduce

theorem add_left_cancel (t a b : nat) : t + a = t + b → a = b :=
begin
  intro h,
  repeat {rw nat.add_comm at h},
end

Expected behavior:

Either give out an error or change the goals to

1 goal
tab: ℕ
h: a + t = b + t
⊢ a = b

Actual behavior:
Does not terminate and the Infoview shows

Loading...

Reproduces how often:
All the time.

Versions

Lean (version 3.30.0, commit a5822ea47ebc, Release)
Windows 10 Home Edition

Additional Information

None.

Start by reproducing the theorem with repeat {rw nat.add_comm at h} in Lean 3.30.0 and observe the Infoview's nontermination. The payload names no source file or test path; done means the tactic either reports an error or reaches the expected single goal instead of remaining on “Loading...”.