Confusing messages if wrong version of Lean vscode extension used.

[EdAyers]

If I open a Lean 4 project in vscode and forget to deactivate the lean 3 extension. The output window pops open with a message Watchdog error: Cannot read LSP request: Invalid header field: .... I've also observed panics in some cases.

This is happening because the Lean 4 server is receiving Lean 3 language server messages.
I think that the user experience could be greatly improved by having both the vscode lean 3 extension and lean 4 be aware of the other protocol and send a friendly message to the user saying that they are using the wrong extension.

[gebner]

It is actually completely supported to have both extensions installed and activated at the same time. I have both installed and it automatically picks the right one depending on the project. Can you give some more info on how to reproduce this bug?

[EdAyers]

I get the Watchdog error whenever the lean4 extension is not enabled.

[EdAyers]

So maybe this should be a core lean issue