Cannot read LSP request: No Content-Length field in header

Stream: lean4

[nicheng0019]

when I execute "lake serve", I get "Watchdog error: Cannot read LSP request: No Content-Length field in header: []", how could I resolve this problem?

[Alissa Tung]

Did you send the message via the lsp process stdin? If so, could you display the concrete message that was sent?

[nicheng0019]

sorry, I am a newbie at lean. I just installed the extension lean4 in the VSCode, and restarted the lean server, but the server failed to start, there was a "Watchdog error: Cannot read LSP notification: invalid argument (error code: 22, invalid argument) " mistake in the output.

So I searched the reason on the internet, and someone said to execute "lake serve". When I executed "lake serve", I got the result above.

[Alex J. Best]

As a user of Lean you shouldn't need to execute lake serve yourself directyl ever

[nicheng0019]

Then how I resolved "Watchdog error: Cannot read LSP notification: invalid argument (error code: 22, invalid argument)" when I used lean4 in VSCode?

[Alissa Tung]

I think what we can do is that

• check the versions of VS Code and Lean 4 toolchain are latest
• check that there is no local software that blocks JSON rpc
• check that if there is more logs, for example, more outputs in the outputs of VS Code bottom panel

[nicheng0019]

Thank you for your reply,

• the versions of VS Code and Lean 4 are latest
• the output of VS Code are: image.png
  
• I will check whether there is some software that blocks JSON rpc