Constant errors from LSP plugin

[gebner]

When editing a Lean 4 file, I am getting the following kind of error very frequently:

LSP[leanls]: Error NO_RESULT_CALLBACK_FOUND: {
  id = 101,
  jsonrpc = "2.0"
}

Sometimes the response is clearly from autocompletion. Is there something obvious that I should be doing?

[Julian]

I've seen this error before but haven't been able to deterministically reproduce it... For me it's happened at most once per session, and rarely (i.e. not in every session).

I think what it means is the server is sending back some message that isn't registered in vim.lsp.handlers -- so either that's something the server shouldn't be sending or something we can put a null handler in there for, but since I haven't been able to deterministically reproduce I haven't been able to check which -- in fact I don't even know what kind of request is being responded to!

So yeah maybe is there anything you can share that deterministically seems to cause this? I'll try to find the spot that we'd need to instrument to debug which LSP request is involved there, I think if we shove a print statement in there it'd tell us what handler we should add to vim.lsp.handlers, if it's in fact a neovim bug.

[gebner]

leanprover/lean4#499

[Julian]

Nice find.

[Julian]

Fixed in leanprover/lean4#506 it seems. Thanks (both for diagnosing and fixing!)