`repeat` with a missing body burns the full heartbeat budget and ~4 GB on a file after a parse error has already been reported

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

A tactic block ending in a bare repeat makes Lean spend the entire default heartbeat budget—about 32 seconds of CPU time and several gigabytes of peak resident memory—on a two-line file after a parse error has already been reported.

The parse error is the only diagnostic printed. Nothing indicates why Lean continues running or where the time and memory went.

Steps to Reproduce

Create test.lean:

example : True := by
  repeat

Run:

$ /usr/bin/time -v lean test.lean
test.lean:3:0: error: unexpected end of input; expected '{'
Command exited with non-zero status 1
        User time (seconds): 24.85
        System time (seconds): 7.11
        Percent of CPU this job got: 96%
        Elapsed (wall clock) time (h:mm:ss or m:ss): 0:33.09
        Maximum resident set size (kbytes): 4549604
        Major (requiring I/O) page faults: 38443
        Exit status: 1

Lean reaches approximately 4.34 GiB of peak resident memory before terminating.

Expected behavior: Lean should report the parse error and exit promptly with a nonzero status.

Actual behavior: Lean reports the parse error, then continues running until the default heartbeat budget is exhausted, consuming CPU and several gigabytes of memory in the process.

Baseline: For comparison, replacing the file with a valid proof:

example : True := by trivial

produces

	Command being timed: "lean test.lean"
	User time (seconds): 0.15
	System time (seconds): 0.12
	Percent of CPU this job got: 15%
	Elapsed (wall clock) time (h:mm:ss or m:ss): 0:01.81
	Maximum resident set size (kbytes): 454476
	Major (requiring I/O) page faults: 54
	Exit status: 0

Version

Reproduced on:

Lean (version 4.32.2, x86_64-unknown-linux-gnu, commit f3b06c705e6c85f5314019d5d3baab0fec5b580c, Release)
Arch Linux

Also reproduced on the latest nightly tested:

Lean (version 4.34.0-nightly-2026-08-06, x86_64-unknown-linux-gnu, commit c4e6b62c3d955ef20da94310797072f7c4c5fa2b, Release)

Nightly result:

test.lean:3:0: error: unexpected end of input; expected '{'
Command exited with non-zero status 1
	Command being timed: "lean +leanprover/lean4:nightly test.lean"
	User time (seconds): 24.21
	System time (seconds): 9.88
	Percent of CPU this job got: 95%
	Elapsed (wall clock) time (h:mm:ss or m:ss): 0:35.59
	Maximum resident set size (kbytes): 3774248
	Major (requiring I/O) page faults: 40377
	Exit status: 1

Additional Information

This is not an infinite loop: the heartbeat limit eventually ends the run.

Lowering the heartbeat limit makes the same file terminate promptly:

set_option maxHeartbeats 1000 in
example : True := by
  repeat

This suggests that the resource cost depends on the configured heartbeat limit. Files or projects that increase maxHeartbeats may therefore experience substantially greater CPU and memory consumption.

The timeout itself is not reported in the incomplete-repeat case. Compare this with a case where no parse error is involved:

set_option maxHeartbeats 1000 in
example : True := by
  repeat skip

This reports:

test.lean:3:9: error: (deterministic) timeout at `«tactic execution»`, maximum number of heartbeats (1000) has been reached

With the bare repeat, only the preceding parse error is printed, so the reason for the roughly 30-second, multi-gigabyte run is not visible to the user.

Start by running the two-line test.lean reproduction with /usr/bin/time -v lean test.lean, then compare it with repeat skip under maxHeartbeats 1000. Trace the bare repeat after the parse error; done means Lean exits promptly, reports the relevant timeout or diagnostic, and avoids the excessive CPU and memory use.