06-07 VSCode Server Bug

Stream: lean4

[Mac Malone]

Attempting to update a project (Lake) from the 06-01 to the 06-07 nightly (on Windows) gives me the following errors when trying to start the server in VSCode:

[Error - 1:17:42 AM] Server initialization failed.
  Message: Pending response rejected since connection got disposed
  Code: -32097
[Error - 1:17:42 AM] Lean 4 client: couldn't create connection to server.
  Message: Pending response rejected since connection got disposed
  Code: -32097

These result in the server crashing and failing to recover regardless of the number of restarts.

[Scott Morrison]

Std4 is already on the 06-07 nightly, and seems to open okay in VSCode

[Mac Malone]

@Scott Morrison Yeah, I was trying to bring Lake to the same version. I just tested std4 on my machine and it to is broken in VSCode.

[Mac Malone]

What version of VSCode are you using Scott? Also did you try opening a Lean file?

[Mac Malone]

I am on 1.78.2

[Mario Carneiro]

std4 works on my vscode, although I was having issues opening the hover.lean test (could be unrelated)

[Mac Malone]

What VSCode / OS version are you using, Mario?

[Mario Carneiro]

$ code --version
1.78.2
b3e4e68a0bc097f0ae7907b217c1119af9e03435
x64

OS is Ubuntu 22.04

[Mac Malone]

Okay, same VSCode version as me but not Windows.

[Mario Carneiro]

vscode-lean4 v0.0.103

[Mac Malone]

I am on 64-bit Windows 10 22H2, VSCode 1.78.2, and vscode-lean4 v0.0.103

[Scott Morrison]

% code --version
1.78.2
b3e4e68a0bc097f0ae7907b217c1119af9e03435
x64

[Scott Morrison]

on macos

[Scott Morrison]

I guess we need to ask for another Windows tester.

[Scott Morrison]

!4#4847 is an attempted bump of mathlib4 to 06-07, it is also fine in VSCode.

[Marc Huisinga]

Scott Morrison said:

I guess we need to ask for another Windows tester.

I created a new Lean 4 project on windows with lean4:nightly-2023-06-07 and the Main.lean that is generated by default loads fine. Same Windows 10 version, VSC and vscode-lean4 as @Mac.

[Marc Huisinga]

... Having built std4 now for a less trivial test, it loads fine as well.

[Mac Malone]

@Marc Huisinga Well that makes this confusing.

[Marc Huisinga]

I am sure some form of state is to blame :grinning_face_with_smiling_eyes: