Very high CPU usage when making any edits at the top of a file

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

When editing at the top of any long Lean file, CPU usage spikes a lot. This is presumbly caused by re-elaborating the entire file on every keystroke. It can be mitigated by placing #exit after the block being edited, but this is very inconvenient.

Context

I use Lean on a laptop, and if my laptop starts to get hot, the keyboard becomes too hot to type on. So this bug makes writing Lean somewhat inconvenient for me – I always have to use #exit whenever I make changes at the top of any file. This is possibly editor-specific, but it also produces input lag, which is annoying.

Steps to Reproduce

1. lake new Reproducer
2. In Reproducer.lean, repeat the line example : Nat := 5 a thousand or so times
3. Start writing a comment at the top of the file
4. Observe your computer fans start to whir, and CPU usage to spike
5. Place #exit after the comment, and continue writing the comment
6. Observe that CPU usage no longer spikes

Expected behavior: I can edit the top of the file without my laptop getting too hot and without having to use #exit.

Actual behavior: CPU usage is very high.

Versions

Lean 4.35.0-nightly-2026-09-03
Target: x86_64-unknown-linux-gnu Linux

Reproduced in both Neovim and VSCode.

Additional Information

A screen recording of the issue. Notice the CPU usage goes from 250% to 6% with #exit.

https://github.com/user-attachments/assets/d82bb307-547d-48e1-8ec4-5ee9e3c0acb7

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start by reproducing the issue with the minimal lake new Reproducer case: repeat example : Nat := 5 about a thousand times, then edit at the top with and without #exit. Trace the work triggered by those edits in both Neovim and VSCode; done means top-of-file editing no longer causes very high CPU usage or input lag without requiring #exit.