feat: use lake serve

[lovettchris]

See Zulip Discussion

Proposal, replace the following setting:

With:

Then the rules for using lake serve would be:

1. is 'lake' or 'lake.exe' found in the toolchainPath, If not don't use lake
2. is there a lakefile.lean in the current workspace root? If not don't use lake
3. If the above are both good, use lake serve with optional +version if there's a workspace override in effect.
4. If lake serve -- args fails fall back on lean --server.

[gebner]

Otherwise lgtm. Let's wait for the lake version bump to land in lean and check that the integration works as expected, then merge.

[lovettchris]

Otherwise lgtm. Let's wait for the lake version bump to land in lean and check that the integration works as expected, then merge.

When will that be, I don't see any Lake PR that is removing the "pre" specialDesc label...

[tydeu]

@lovettchris my hope is to get it done this weekend, now that I have finished with other obligations that had been occupying my time.

[lovettchris]

@gebner I merged this with master, but it was a nasty merge, so will need thorough testing.

[lovettchris]

@gebner - another tricky merge with master. We both changed ensureClient to take a Uri, but the new version also returns a boolean telling caller if this was a new client or a cached client, needed in the implementation of installChanged. So anyway, I tested it on a multi-workspace situation and it seems to work, the latest build of Lean now has "Lake 3.0.0" and so lake is now showing up in the ps trace, and you can mix and match, here's a multi-workspace with one using older version of lean so it's running "lean --server" directly, while the other is using Lake. Nice.

Code.exe: "Code.exe" .
  Code.exe: "Code.exe" --ms-enable-electron-run-as-node --nolazy --inspect-brk=53727 "resources\app\out\bootstrap-fork" --type=extensionHost --skipWorkspaceStorageLock
    cmd.exe: C:\WINDOWS\system32\cmd.exe /d /s /c "lean --server d:\Temp\lean_examples\test"
      lean.exe: lean  --server d:\Temp\lean_examples\test
        lean.exe: "leanprover--lean4---nightly-2022-01-20\bin\lean.exe" --server d:\Temp\lean_examples\test
          lean.exe: leanprover--lean4---nightly-2022-01-20\bin\lean.exe "--worker" "file:///d%3A/Temp/lean_examples/test/Test.lean"
    cmd.exe: C:\WINDOWS\system32\cmd.exe /d /s /c "lake serve -- d:\Temp\lean_examples\Foo"
      lake.exe: lake  serve -- d:\Temp\lean_examples\Foo
        lake.exe: "leanprover--lean4---nightly\bin\lake.exe" serve -- d:\Temp\lean_examples\Foo
          lean.exe: leanprover--lean4---nightly\bin\lean.exe "--server" "d:\Temp\lean_examples\Foo"
            lean.exe: leanprover--lean4---nightly\bin\lean.exe "--worker" "file:///d%3A/Temp/lean_examples/Foo/Main.lean"

[lovettchris]

I am seeing one interesting warning when I remove a folder from my multi-folder workspace:

Watchdog error: Got `shutdown` request, expected an `exit` notification

Do you know what LSP is talking about?

[Vtec234]

@lovettchris : according to the LSP spec, after the client sends a shutdown request it should follow that up with an exit notification but not anything else inbetween. So I'm guessing the client actually does send something else, which a spec violation. It would be better to print out the actual message received here. We could also make the server ignore this, but I rather keep it spec-compliant and fix the client.

[tydeu]

@lovettchris A general note: In elan paralance, the toolchain path is to the root directory (sysroot) of the toolchain (e.g., leanprover--lean4---nightly), not the bin directory of the toolchain. So VSCode should ideally be using the executables at <toolchainPath>/bin.

[lovettchris]

@lovettchris A general note: In elan paralance, the toolchain path is to the root directory (sysroot) of the toolchain (e.g., leanprover--lean4---nightly), not the bin directory of the toolchain. So VSCode should ideally be using the executables at <toolchainPath>/bin.

Done. But in testing this things are going a bit wonky, I tried debugging it but got stuck, so I would love your help. It seems now that when I use SelectToolchain to select a different version, or a custom path, the lean server restarts no problem, I get "running" state and the pstree shows the right version of lean.exe is running, but any change to a .lean source file returns an error saying:

Watchdog error: cannot find open document 'file:///d%3A/Temp/lean_examples/Foo/Main.lean'
[Info  - 8:57:59 PM] Connection to server got closed. Server will restart.
Watchdog error: cannot find open document 'file:///d%3A/Temp/lean_examples/Foo/Main.lean'
[Info  - 8:58:00 PM] Connection to server got closed. Server will restart.

Here are the log files for the newly restarted lean server (started with lake serve):

logs.zip

I have no idea why a newly created lean client things the file is closed. It is not closed... Interestingly, if I do a Developer: Reload Window command then everything works fine on the newly selected version... but a Lean4: Restart Server command does not fix it. So some sort of weird residual thing going on...

[lovettchris]

Update: there's huge merge conflicts between this PR and fix: #115 : Infoview not working for external file so I'm going to pre-empt that mess, and re-apply the changes in this PR on top of that PR carefully checking every line and perhaps that will solve this weird problem I'm running into here.

[lovettchris]

Indeed, re-applying the changes on top of #117 solved the problem.