Lean 4 server crashing

[rish987]

Hey, I've just started using Lean 4 and often get the error:

Client 1 quit with exit code 1 and signal 0

when I start editing. Not sure if it's related to #203? Just wanted to ask if you've ever seen this and know what's up, if not LMK if there's any more info I can provide to help find the issue. I didn't see any output in ~/.cache/nvim/{log,lsp.log}, though I could also try to get a core dump.

[Julian]

I don't think I've seen this before but I've used Lean4 less recently -- what version are you on just to be sure? And nothing on stderr when this happens?

[rish987]

leanprover/lean4:nightly-2022-05-18 and NVIM v0.8.0-dev+302-gaf2899aee (sorry, that should have been the first thing I included here)

Yeah I don't see any other output, the server just silently fails. Since you haven't seen this it very well may be my problem, I'll try things within an isolated environment tomorrow and get back to you.

[rish987]

Hmm yeah one of my plugins may be messing things up, I have no issues editing with make nvim. I'll try to figure out which one it is. Also just got this stderr output for the first time on a recent crash:

Watchdog error: Got outdated version number

[gebner]

This looks like your Lean installation is messed up a bit. When you start lean from nvim, it runs lean --server, which in turns runs one lean --worker process per file. The error means that these two processes come from different Lean versions.

EDIT: Sorry, the error means something else.

[rish987]

Aha, it's completion related. I'm using nvim-cmp and see a crash (with the watchdog error above) inconsistently when invoking completion and then entering a newline. Not sure where the error lies, but I guess I can do without completion for now until I have time to look deeper.

[Julian]

I'm on a similar setup (and I think so is Gabriel) so will keep thinking I suppose about anything that might be different -- dropping your LSP log to trace via vim.lsp.set_log_level("TRACE") may be a thing to try perhaps to see what LSP method might be happening just before the exit?

[Julian]

I've now actually seen this (on Lean (version 4.0.0, commit 3eeeca22e281, Release)) where I got a notification that:

2022-06-27T11:57:27  WARN Client 1 quit with exit code 1 and signal 0

but nothing on stderr and nothing else in :messages. I was doing nothing particularly special while that happened (just editing some unremarkable structure).

It should be that this is an upstream issue though right, so we should probably take it there if/when we diagnose this.

[rish987]

OK good to know, yes I can confirm that I'm still seeing crashes as well without autocompletion, but they've become much less frequent. Hopefully the problem with completion is related because it's pretty easy for me to reproduce.

[rish987]

So I think this could be coupled with synchronization issues (i.e. the server not picking up changes correctly) which I've noticed as well. I suspect the issue is on the nvim side, will investigate.

[rish987]

I've investigated a bit more into my config, and I think this has to do with runtime load triggering a timing-related synchronization issue. In my case, I had a line require("luasnip.loaders.from_vscode").load() that loaded a ton of snippets from the friendly-snippets plugin, and commenting that out made the issue disappear (and made my nvim instance run faster in general) -- that's not to say that it fixed the issue, it probably just made it much less likely to occur. I will investigate further.

[rish987]

We're debouncing. It turns out that because neovim flushes pending changes on every server request, we're getting multiple textDocument/didChange notifications with the same version number (but different contents, the latter ones being empty) due to an upstream bug. And I think we're the only ones who manually issue server requests often enough to notice it (which explains why I only saw this crash with the infoview open). neovim/neovim#19314 should fix it!

[rish987]

I think we can close this now, my only concern is that @Julian saw crashes without the Watchdog error: ... stderr output. And I think I've had this as well much earlier on, but recently I've only been getting a crash along with that output, I wonder if it could have something to do with the toolchain? But then again it looks like this line has been there for quite a while. I'd say we should leave this open for a bit more just to see if there are any other random crashes.

[Julian]

I think we're also seeing something similar to this in CI, but I haven't gotten a chance to debug (well done tracking this down!). But yeah clients in CI seem to just exit with no output, but only on neovim nightly, stable is fine, and nightly I can't reproduce locally even :/

[Julian]

OK gonna close this now since I haven't seen it recently and whatever was happening in CI isn't happening anymore, but lemme know if someone still does see these.