Extension error message

Stream: lean4

[Patrick Massot]

Today my VScode keeps opening the output panel at the bottom with errors Cannot send message to unknown document... mentioning existing files. Everything works but it's very annoying that this bottom panel keeps opening like this.

[Patrick Massot]

Is this a known issue?

[Arthur Paulino]

I've been experiencing this for a while

[Alastair Horn]

I find it sometimes happens when I close a file I was editing, it's fine when I restart vscode though

[Gabriel Ebner]

This is probably the same class of bug as https://github.com/leanprover/lean4/issues/1219 aka race conditions because we don't even have mutexes.

[Gabriel Ebner]

See also https://github.com/leanprover/lean4/issues/1280

[Gabriel Ebner]

W.I.P.

[Sebastian Ullrich]

I'm not saying there's no chance of race conditions, but the references to having to restart VS Code make me think the editor and watchdog fundamentally disagree about what files are open, persistently. Does VS Code even send didOpen requests after restarting the language server? I know the LSP says it doesn't have to since requests to closed files are allowed.

[Gabriel Ebner]

It could also be the infoview sending RPC messages to closed files. @Patrick Massot @Arthur Paulino Please open bugs with the full error message.

[Sebastian Ullrich]

Would also help to have a new release that includes https://github.com/leanprover/vscode-lean4/pull/229

[Wojciech Nawrocki]

Gabriel Ebner said:

It could also be the infoview sending RPC messages to closed files. Patrick Massot Arthur Paulino Please open bugs with the full error message.

The messages I am seeing are exactly this, they are keepAlives for closed files.

[James Gallicchio]

(fwiw, restarting vs code doesn't resolve the issue for very long for me...)

[James Gallicchio]

(if at all? unclear)

[Patrick Massot]

@Gabriel Ebner in which repo do you want a bug report? The full error message is:

Cannot send message to unknown document 'file:///home/pmassot/lean/lean4tests/TermUnsafe.lean':
{"params":{"uri":"file:///home/pmassot/lean/lean4tests/TermUnsafe.lean","sessionId":"5236639616267868746"},"method":"$/lean/rpc/keepAlive","jsonrpc":"2.0"}

[Wojciech Nawrocki]

This might do it

[Gabriel Ebner]

@Patrick Massot The vscode-lean4 repo is the place to complain. If it's a server issue I can easily transfer it to the main repo.

[Patrick Massot]

It seems that errors are gone but everything became much slower. It may be a problem with my project, but I thought I should report it in case anyone else sees it.

[Gabriel Ebner]

@Patrick Massot Was the slowness already an issue with 0.0.88? The last 0.0.89 release is a tiny change which only takes effect if you close a file or restart the server.

[Patrick Massot]

I think it was unrelated. When I copied my code to a new project to create a MWE I no longer had any issue. And yesterday afternoon it seemed fast again. I still get a lot more transitory error messages in Lean 4 than in Lean 3 when playing with several files. This is probably strongly related to the "refresh file dependency" story.

[Sebastian Ullrich]

Transitory in what way? The main motivation for the explicit refresh action was to avoid spontaneous recompilation.

[Patrick Massot]

They are very hard to reproduce. I'll try to copy error messages here when they come up.

[Patrick Massot]

I don't have much Lean time this morning but I'll probably come back later.

[Chris Lovett]

I think it's all related to recent infoview changes, and we are tracking it with this issue: https://github.com/leanprover/vscode-lean4/issues/235. New code was added that reports LSP error codes -32901 and -32902, I think the infoview is reporting too many errors after file is closed. So I have this proposed fix: https://github.com/leanprover/vscode-lean4/pull/238

[Patrick Massot]

One way to get a confusing extension error message is simply to try to import a file containing an error. The main display becomes either

Error updating: Error fetching goals: Rpc error: RpcNeedsReconnect: Outdated RPC session. Try again.

or

Error updating: Error fetching goals: Rpc error: InvalidParams: Incorrect position 'file:///tmp/issue/Main.lean:3:16' in RPC call. Try again.

[Patrick Massot]

Putting the cursor on the import line gives a slightly less confusing error message, but not great either.

[Patrick Massot]

I opened https://github.com/leanprover/vscode-lean4/issues/239 with more details.