lean in neovim stalls

Stream: lean4

[Antoine Chambert-Loir]

Since a few weeks, lean in neovim doesn't work well for me, any significant modifications leands neovim to indicate that it is Processing file, but that seems to take hours… Doing LeanRestartFile each time kind of works, but this is quite painful. Moreover lake build … works swiftly, so it does not seem to be lean/lake, but really neovim.

I tried to update the plugins, with no significant output.

[Patrick Massot]

@Julian Berman :up:

[Julian Berman]

@Antoine Chambert-Loir is there anything else notable about the project this happens with? Is it Mathlib? Does it happen if you don't import anything, and then happens if you import Mathlib? Also perhaps share :checkhealth lean though I doubt it will have anything notable in it.

[Antoine Chambert-Loir]

Here is the output of :checkhealth lean; it seems OK…

  lean.nvim
  - OK Neovim is new enough.
  -   vim.version():  0.10.2
  - OK Lake is runnable.
  -   lake --version:  Lake version 5.0.0-01d414a (Lean version 4.13.0-rc3)

[Antoine Chambert-Loir]

In case it helps, here is the error message I get:

LSP[leanls]: Error NO_RESULT_CALLBACK_FOUND: {
  error = {
    code = -32601,
    message = "No RPC method 'Lean.Widget.getInteractiveDiagnostics' found"
  },
  id = 2528,
  jsonrpc = "2.0"
}

[Antoine Chambert-Loir]

(with ids increasing from that to 2692, …, 2766,…)

[Julian Berman]

OK, I've seen that error (and have been working on it). I'll get back to it today and should have a fix for you to update to. I'm intrigued that no one else sees it besides you and me, but maybe others see it and haven't reported it yet.

[Patrick Massot]

I’m pretty sure I’ve already seen it, but not in a reproducible way.

[Julian Berman]

The reproducible way that I know of is if your file starts with import Foo and then you try to edit near it, and Foo is nonsense (i.e. the import doesn't exist or isn't valid syntax or something) and then you try to edit around there, then Lean sends back messages saying "I'm dead, stop!" and doesn't respond to that RPC method.

[Julian Berman]

So I think I know how to fix it, I'm just confirming. And then hopefully that's the case that the two of you have seen.

[Julian Berman]

I have been busier than expected the last few days so I haven't pushed this out yet, apologies, but just noting I definitely haven't forgotten about it.

[Julian Berman]

Even though I still don't really understand this scenario well enough to be able to reproduce it in an automated test, I've just pushed out what fixes it for me in the case I was aware of. If you update please let me know if it doesn't fix things for you.

[Julian Berman]

No rush of course but @Antoine Chambert-Loir did this fix things for you hopefully?

[Antoine Chambert-Loir]

I hadn't the opportunity to do much Lean in the present days. On thursday, the few modifications I made seemed that it was better, but I remember having gotten a few of this “No RPC method” error. (A few within one hour of coding, and not one after every modification.)