leanprover/lean4

question: why wait for `initialized` is needed here?

Opened this issue · 1 comments

alissa-tung commented

See

lean4/src/Lean/Server/Watchdog.lean

Line 1047 in 1c20b53

discard $ st.hIn.readLspNotificationAs "initialized" InitializedParams

in some async language server implementation, for example, async-lsp, client may response the register_lean_watcher request (register_ilean_watcher) before sending initialized notification. So the client side router should take care of the sequence of messages, first sending initialized, then response the register_lean_watcher

mhuisi commented

Thanks for the bug report. We should probably just send the watcher requests after the initialization dance is done so that this race condition cannot occur.