Severe lag: repeated $/lean/rpc/call request storm in <1s

[yd278]

Hi, I’m seeing severe lag specifically while typing in Lean files.

From Neovim’s LSP log, there is a “request storm” where the client repeatedly sends identical $/lean/rpc/call requests (e.g., Lean.Widget.getWidgets / Lean.Widget.getInteractiveTermGoal) to the same position dozens of times within less than one second.

Additionally, Lean’s built-in Unicode input is very slow in this setup: typing “\in” at the end of the line and waiting for it to convert to “∈” takes a long time.

Environment:

• Neovim: 0.11.2

• lean.nvim: latest

• Lean toolchain: Lean 4.24.0 (arm64-apple-darwin23.6.0), commit 797c613eb9b6d4ec95db23e3e00af9ac6657f24b, Release

• OS: macOS 15.6.1 (24G90)

• Plugin manager: lazy.nvim

Minimal reproducible setup:

• Plugins enabled:

  • lazy.nvim
  • lean.nvim
  • nvim-lspconfig
  • plenary.nvim

• File: section_3_1.lean (https://gist.github.com/yd278/15437d60c8b068b148373e0914facb6b)

• Steps:

  1. Open the file and go to around line 283. Wait until the server finish processing the file.

  2. Type “\in” at the end of the line (use Lean’s Unicode input).

  3. Observe that converting to “∈” takes a long time, and the editor becomes laggy.

  4. LSP log shows many identical $/lean/rpc/call requests within <1s to the same position.

Comparison with VS Code:

• Running the same file and performing the same typing (“\in” → “∈”) in VS Code does not lag.

• This suggests the issue is likely in the Neovim client side (lean.nvim integration or event handling), rather than the language server itself.

Observed behavior:

• During typing, Neovim rapidly issues many identical $/lean/rpc/call requests in under a second, causing noticeable lag.

• Unicode input (“\in” → “∈”) conversion is particularly slow.

Expected behavior:

• Requests should be debounced/merged; typing (including Unicode sequences) should not cause a storm of identical RPC calls or noticeable lag.

Logs:

• Neovim LSP log excerpt attached

debug.log