Cannot send message to unknown document

Stream: lean4

[Alexander Bentkamp]

Any ideas where this message could come from?

Cannot send message to unknown document 'file:///home/alex/Projects/verified-optimization/code/DCP/DCP/Syntax/ProblemMacroMData.lean':
{"params":{"uri":"file:///home/alex/Projects/verified-optimization/code/DCP/DCP/Syntax/ProblemMacroMData.lean","sessionId":"7188571717961512369"},"method":"$/lean/rpc/keepAlive","jsonrpc":"2.0"}

I am on lean4:nightly-2021-10-18, VSCode, Ubuntu. These messages pop up constantly in VSCode's "Output" panel.

[Gabriel Ebner]

Does this happen after restarting the lean server?

[Alexander Bentkamp]

Unfortunately restarting the lean server does not help

[Gabriel Ebner]

That was not my question.

[Gabriel Ebner]

My question was: "did you restart the server before the problem occurred"

[Alexander Bentkamp]

Oh, sorry. Yes it does appear directly after restarting the server, but then continues to pop up, e.g. when hovering over certain parts of Lean code.

[Gabriel Ebner]

Ah, then it's presumably the same issue as https://github.com/Julian/lean.nvim/issues/189

[Alexander Bentkamp]

Ok, right, it really happens only after a restart or after "Refresh file dependencies"

[Alexander Bentkamp]

I'll try to avoid them for now :-)

[Gabriel Ebner]

You can also use "Reload window" for now.