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

Aperta
  • Qualcosa non va?
#442 1 commento 4 reazioni 0 assegnatari Vedi su GitHub

I maintainer di solito rispondono entro 1 giorno

Nessuno ha ancora preso questa issue.

Valutazione

Difficoltà
4/5
Tempo stimato
3-5 giorni
Idoneità per principianti
42/100
Tipo di issue
Bug
Chiarezza
Abbastanza chiara
Stato di attività
Tranquilla
Stack tecnologico
lua, neovim
Ambito
tooling

Direzione di ricerca

Riproducete il rallentamento in section_3_1.lean intorno alla riga 283 con i plugin Neovim indicati e ispezionate il debug.log allegato alla ricerca di richieste $/lean/rpc/call ripetute. Iniziate tracciando l’integrazione di lean.nvim o la gestione degli eventi di Neovim durante l’inserimento di “\in”, quindi verificate che le richieste identiche siano sottoposte a debounce o unite e che la conversione Unicode non causi più un rallentamento evidente.

Scritto dal modello di indicizzazione a partire dal testo della issue.

Descrizione

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

Lingua principale
Lua
Stelle
616
Fork
63
Merge medio
1g 7h
PR unite (30g)
10

Preparare l'ambiente

Come iniziare

  1. Leggi tutta la issue e poi la guida ai contributi del progetto.
  2. Commenta sulla issue per dire che te ne occupi tu — evita che due persone facciano lo stesso lavoro.
  3. Fai un fork del repository e lavora su un branch.
  4. Apri una pull request che faccia riferimento al numero della issue.

Altre issue di Julian/lean.nvim

Tutte le issue di Julian/lean.nvim

Issue simili

Altre issue su Lua

Ricevi le nuove issue nella tua casella

Un breve riepilogo di issue GitHub adatte ai principianti.