Server crashes on new file

Stream: lean4

[Bhavik Mehta]

My Lean server either crashes or doesn't update at all whenever I create a new file. Here's an example error log:

Watchdog error: cannot find open document 'file:///Users/bmehta/Documents/lean/carleson/Carleson/blank.lean'
[Error - 14:26:07] Client Lean 4: connection to server is erroring. Shutting down server.
[Error - 14:26:07] Sending document notification textDocument/didChange failed
Error: Cannot call write after a stream was destroyed
    at new NodeError (node:internal/errors:406:5)
    at _write (node:internal/streams/writable:380:11)
    at Socket.Writable.write (node:internal/streams/writable:393:10)
    at /Users/bmehta/.vscode/extensions/leanprover.lean4-0.0.168/dist/extension.js:1:606745
    at new Promise (<anonymous>)
    at a.write (/Users/bmehta/.vscode/extensions/leanprover.lean4-0.0.168/dist/extension.js:1:606663)
    at y.doWrite (/Users/bmehta/.vscode/extensions/leanprover.lean4-0.0.168/dist/extension.js:1:594277)
    at /Users/bmehta/.vscode/extensions/leanprover.lean4-0.0.168/dist/extension.js:1:594172
[Error - 14:26:07] Connection to server got closed. Server will not be restarted.
[Error - 14:26:07] Sending document notification textDocument/didChange failed
Error: Cannot call write after a stream was destroyed
    at new NodeError (node:internal/errors:406:5)
    at _write (node:internal/streams/writable:380:11)
    at Socket.Writable.write (node:internal/streams/writable:393:10)
    at /Users/bmehta/.vscode/extensions/leanprover.lean4-0.0.168/dist/extension.js:1:606745
    at new Promise (<anonymous>)
    at a.write (/Users/bmehta/.vscode/extensions/leanprover.lean4-0.0.168/dist/extension.js:1:606663)
    at y.doWrite (/Users/bmehta/.vscode/extensions/leanprover.lean4-0.0.168/dist/extension.js:1:594277)
    at /Users/bmehta/.vscode/extensions/leanprover.lean4-0.0.168/dist/extension.js:1:594172

I've had this on 4.9.0-rc1 and 4.9.0-rc2, in different projects, and on different machines with different OSes and different installation setups. It reproduces for me on gitpod too.
Here are the steps I take to reliably crash Lean on my usual setup

1) Have a running Lean server, working on a Lean file
2) Open a new file in VSCode in the same directory
3) Save it as test.lean
4) Write example : 1 = 1 := rfl in the file
5) Save the file
6) Lean server crashes

Doing the same thing on gitpod, but with 1 = 2 in place of step 4 gives no error and no changes in the infoview. Both of these are solved by restarting lean, but this usually has a big time cost.

How can I debug this further?

[Ruben Van de Velde]

Same here

[Marc Huisinga]

The error should only occur before rc2, but I can reproduce that the language server doesn't work on the file when using rc2 (i.e. the Gitpod case you mention). I'll investigate.

[Marc Huisinga]

Looks like this is another edge case in the series of VS Code bugs and API deficiencies that lead to vscode-lean4#460.
Apparently, in this particular way of opening documents, VS Code does not update the window.tabGroups field before the language client library attempts to send a didOpen request to the server, so we conclude that it is one of those "invisible" Lean documents that VS Code sometimes tries to open in the background that we don't want to spam the language server with.
I'm not sure how to fix this yet. window.tabGroups is the closest approximation I know of to filter the invisible documents that VS Code often attempts to open, but it doesn't allow us to distinguish the new document in this case from actual invisible documents. VS Code doesn't provide any alternative API to deal with this issue, either.

I'll think some more about it tomorrow, but the workaround for this on rc2 is that you can close test.lean and then re-open it. Then, when the language client attempts to open the document, VS Code will already have updated window.tabGroups.

[Bhavik Mehta]

I see, thanks for the workaround. I would make an issue for this but I don't know enough about the actual cause to be able to explain it properly, would you mind?

[Marc Huisinga]

Bhavik Mehta said:

I see, thanks for the workaround. I would make an issue for this but I don't know enough about the actual cause to be able to explain it properly, would you mind?

An issue with the reproduction steps above and a link to this thread is perfectly sufficient!

[Bhavik Mehta]

It should be an issue on vscode-lean4 rather than lean4 itself right?

[Marc Huisinga]

Yes, the problem is VS Code being broken and vscode-lean4 desperately and insufficiently trying to work around it. The language server is doing the right thing here.

[Bhavik Mehta]

https://github.com/leanprover/vscode-lean4/issues/484

[Marc Huisinga]

Since I don't really see a way forward to fix this issue on our end at the moment in a way that meets all requirements, I've asked the VS Code developers for clarification. Let's see what comes of this; the most likely way forward that I see is that VS Code fixes whatever issue causes window.tabGroups to not be up-to-date here.

[Bhavik Mehta]

I seem to still get (a milder version of) this, where I open an existing file but the server doesn't seem to register it. Closing the file and re-opening it doesn't help, only restarting the server with the second file open works. Is there a workaround better than restarting the server? I presume it's the same root cause as the above

[Bhavik Mehta]

rc2, v0.0.169, macOS

[Kim Morrison]

Can you give a repro?

[Bhavik Mehta]

1) Have file open with Lean working as normal
2) Open a different, existing file
3) About 30% of the time, for me, the info view doesn't react to the new file, including no errors on obvious problems

[Marc Huisinga]

When this happens, is there an error in the debug console? (Ctrl+Shift+P > Developer: Toggle Developer Tools, and then the output in the "Console" tab)

[Bhavik Mehta]

I don't think so, but I will double check later today.

[Kim Morrison]

@Bhavik Mehta, is this in gitpod? If not, which OS? I think we're going to have to get more specific about your system to be able to help here.

[Bhavik Mehta]

MacOS monterrey, version 12.5

[Bhavik Mehta]

Marc Huisinga said:

When this happens, is there an error in the debug console? (Ctrl+Shift+P > Developer: Toggle Developer Tools, and then the output in the "Console" tab)

Just double checked, and there's no error in the debug console.

[Bhavik Mehta]

Please let me know if there's any other debug information I can provide!

[Bhavik Mehta]

I just had it on gitpod too - opening a new file from cmd-click an import, and the infoview has no reaction

[Bhavik Mehta]

Kim Morrison said:

Can you give a repro?

Hopefully this helps: https://www.youtube.com/watch?v=2z-0eypIQuk

[Marc Huisinga]

Hmmm. DId you ever encounter this issue when not using SSH?

[Bhavik Mehta]

Yes, it also happens for me locally (that's what the original macos, rc2, v0.0.169 was referring to)

[Bhavik Mehta]

Most frustrating is the fact that closing the (second) file and re-opening it doesn't make the infoview respond, neither does closing the second file and restarting the server; nor closing the second file and reloading vscode. The only fix seems to be to restart the server after opening the second file, which means I need to restart the server about one in every three files I open and want to get any information for. As an aside, this means I'm finding the #align statements really useful to tell me what the right namespace is to use a lemma, since Lean can't tell me this!

[Damiano Testa]

I have experienced this as well (on Linux): I restart the server fairly frequently.

[Kim Morrison]

I can reproduce this in gitpod!

[Kim Morrison]

(Works fine locally)

[Bhavik Mehta]

Is there any further information I can give to help debug the local issue?

[Marc Huisinga]

Bhavik Mehta said:

Is there any further information I can give to help debug the local issue?

I still can't reproduce the issue myself (I have a suspicion that it has to do with latency, and perhaps I'm just too close to the GitPod servers), but I'm preparing a custom version of the extension for you to try so that we can figure out whether it has something to do with VS Code having additional bugs related to tabGroups, perhaps some which are affected by latency.

[Marc Huisinga]

@Bhavik Mehta
lean4-0.0.171.vsix

1. Go to a fresh Gitpod instance and open your desktop VS Code instance like you did in the video.

2. Navigate to the Extensions menu and select "Install from VSIX" and then "Show local"
   image.png

   

3. After installing the VSIX, when VS Code offers to reload the window, reload it.

4. Confirm that the extension is installed by checking whether the version of the extension in the list of SSH extensions is 0.0.171
   image.png

   

5. See if you can still reproduce the issue with this extension version.

Since VS Code caches these VSIX files sometimes, it may be difficult to uninstall this Lean 4 extension version later, so you should ideally do this on a disposable Gitpod instance just to be safe.

Thanks for your patience.

[Bhavik Mehta]

This does indeed seem to fix it on gitpod - I haven't tried locally because of the vsix cache issue you mentioned!

[Marc Huisinga]

Bhavik Mehta said:

This does indeed seem to fix it on gitpod - I haven't tried locally because of the vsix cache issue you mentioned!

That's great to hear, even though this confirms that VS Code's tab API is practically broken (and to be honest, I still don't understand how it manages to be broken in such a non-deterministic manner). Since the current state of the discussion at vscode-languageserver-node#848 seems to be that the tab API being broken is intended behavior, I don't think this will change soon, either.

I think we may just need to take the potential performance hit that the language server will occasionally start processing invisible files in the background when using Ctrl+Hover and add some additional debouncing for the language server in future Lean versions so that this is less likely to occur from that point onwards. I'll release the fix on Monday after @Kim Morrison has confirmed that it also reliably fixes the issue on their setup.

[Kim Morrison]

Sorry for the slow confirmation, but yes, this also fixes it for me in gitpod!

[Marc Huisinga]

The fix for both of the issues reported above has now been released as part of 0.0.171.