Severe lag: repeated $/lean/rpc/call request storm in <1s
Nobody has claimed this yet.
Assessment
- Difficulty
- 4/5
- Estimated time
- 3-5 days
- Newbie friendliness
- 42/100
Research direction
Reproduce the lag in section_3_1.lean around line 283 with the listed Neovim plugins and inspect the attached debug.log for repeated $/lean/rpc/call requests. Start by tracing the lean.nvim integration or Neovim event handling during “\in” input, then verify that identical requests are debounced or merged and Unicode conversion no longer causes noticeable lag.
Written by the indexing model from the issue text.
Description
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:
-
Open the file and go to around line 283. Wait until the server finish processing the file.
-
Type “\in” at the end of the line (use Lean’s Unicode input).
-
Observe that converting to “∈” takes a long time, and the editor becomes laggy.
-
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
- Dominant language
- Lua
- Stars
- 607
- Forks
- 63
- Avg merge
- 1d 8h
- Merged PRs (30d)
- 8
Getting set up
- No Dockerfile or Docker Compose file
- No pull request template
- Read the contributing guide
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
More from Julian/lean.nvim
-
Difficulty 2/5 1-3 hours Newbie friendliness 70/100
-
Difficulty 2/5 1-3 hours Newbie friendliness 88/100
-
Difficulty 3/5 1-2 days Newbie friendliness 56/100
-
Difficulty 4/5 3-5 days Newbie friendliness 48/100
-
Difficulty 3/5 1-2 days Newbie friendliness 58/100
All issues in Julian/lean.nvim
Similar issues
-
Difficulty 2/5 1-3 hours Newbie friendliness 90/100
Maintainers usually reply within 1 day
-
Difficulty 2/5 1-3 hours Newbie friendliness 78/100
windwp/nvim-ts-autotag#266 ·
-
Difficulty 2/5 1-3 hours Newbie friendliness 78/100
folke/sidekick.nvim#362 ·
-
Difficulty 2/5 1-3 hours Newbie friendliness 72/100
pterodactyl/game-eggs#657 ·
-
enhancement good first issue
Difficulty 2/5 1-3 hours Newbie friendliness 65/100
stalker57241/tabview#10 ·