Would lsp server quit anomaly?

Stream: lean4

[Shanghe Chen]

Hi using a lsp client (namely lsp4ij) connecting lean lsp server I occasionally saw two initialize requests sending to the server like:
image.png
The red part indicates that there is no response for the $/lean/rpc/connect request and the client recreate a initialize request. And the concrete error seems to be java.io.IOException: The pipe is being closed (the Chinese character), which should mean that the input/output pipeline connecting to the server is being closed. Would the reason be the lsp server quiting anomaly? I am not sure it's raised from the lsp server end or lsp client end hence in fact I created also a discussion in here too

[Julian Berman]

Somewhat as usual for your questions, I don't have something specific to help you, but I can say I've noticed some funny initialization behavior in lean.nvim as well, but haven't had time to look into it yet -- specifically I've noticed multiple initialization requests getting sent on startup. Again I have no further info, but I do have a local note reminding me "if you insert vim.print early on you see Lean's LS respond empty a few times" -- so yeah it's possible there's something cross-client happening.

[Shanghe Chen]

Thanks Julian! Yeah I don’t know if it’s because sending $/lean/rpc/connect too early. I saw that the pid of the server changed though. But mostly after some retries it will setup correctly. Hence maybe not a problem but trying to see if there is some log from the server side.