Infoview stalls with message "Waiting for Lean server to start..."

[nateyazdani]

Hello!

I've been following the Lean 4 development on my arm64 macOS system for some time now without much trouble by locally compiling both elan and lean4, and until just recently, everything has worked swimmingly. Unfortunately, I have hit a wall trying to diagnose what has broken recently, causing the infoview to stall indefinitely with the message "Waiting for Lean server to start...". The VSCode output log reports nothing except my toolchain versions: elan 1.3.2-pre (2ab7218e1 2022-02-04) and Lean (version 4.0.0, commit 0649e5fa8ac7, Release).

Any guidance or advice on how I can debug this problem would be greatly appreciated!

Edit:
I'm attempting to follow the instructions for local development+debugging of vscode-lean4 itself, and I saw a potentially interesting line in the debug console: ### error opening document: TypeError: undefined is not iterable (cannot read property Symbol(Symbol.iterator)) [vscode-lean4/src/utils/clientProvider.ts:140]. When I comment out the exception handler, the debug console shows the full stack trace attached here: console.log.

[nateyazdani]

Follow up: I have figured out that the bug I'm experiencing was introduced in vscode-lean4 v0.0.64. I have confirmed that v0.0.60, v0.0.61, v0.0.62, and v0.0.63 all work successfully.

I think that the specific commit at fault here is fa2b871a7ca2a1c6b05655cfe07aed243a8cb1ff . Perhaps the ClientProvider class is somehow surprised by the set of toolchains reported by elan? On my system, elan show outputs the following:

installed toolchains
--------------------

lean (default)
lean-bootstrap

active toolchain
----------------

lean (default)
Lean (version 4.0.0, commit 0649e5fa8ac7, Release)

where "lean" is linked to the build/release/stage1 directory under my checkout of lean4 (and similarly "lean-bootstrap" is linked to the build/release/stage0 directory).

[SquidDev]

I also hit this yesterday, and my understanding of this is that if the extension can't find a workspace root (so a lean-toolchain file), a lot of the code for launching Lean chokes and errors - creating such a file resolves the problem.

I think part of the underlying problem here is that there's a couple of places where the the workspace/folder URI is annotated as non-null, but passed a null/undefined value. Unfortunately TS doesn't detect this unless it's in strict mode - it's possibly worth turning this on across the project, though not quite sure how much work that'd be.

[nateyazdani]

Aha! Creating a lean-toolchain file indeed enables the latest version of the vscode extension to use my installation.

Weirdly, I have to restart the language server once per open Lean source file in order to get its symbol outline, but that's a comparatively minor, probably unrelated glitch in the extension. Thanks for the tip!

I will leave this issue open for now, in case the maintainers want to investigate this behavior further (with which I am glad to help). If they don't, then I'm content to close the matter with this straightforward workaround.

[nateyazdani]

This bug was also discussed on Zulip: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/VSCode.20.22Waiting.20for.20lean.20server.20to.20start.2E.2E.2E.22/near/271659253

[gebner]

Can you try again with 0.0.67?

[gebner]

I think part of the underlying problem here is that there's a couple of places where the the workspace/folder URI is annotated as non-null, but passed a null/undefined value. Unfortunately TS doesn't detect this unless it's in strict mode - it's possibly worth turning this on across the project, though not quite sure how much work that'd be.

Yes, that's a good idea. I believe we already enable strict mode for most of the extension (such as the infoview); but for some reason not for the main extension.

[lovettchris]

Fixed more related bits with opening adhoc files in #127

[nateyazdani]

Sorry to not write back sooner -- have been terribly sick the last few days. I just wanted to confirm that v0.0.67 does indeed resolve this problem on my end. Thanks a bunch!

[lovettchris]

Sorry to hear that Nathaniel, I hope you get to feeling better soon. Please try version v.0.0.68.

[nateyazdani]

Just confirmed that v0.0.68 also maintains the fixed behavior. Thanks again!

[lovettchris]

Great, thanks for confirming. Can you post the output of elan toolchain list from your machine?

[nateyazdani]

Certainly:

$ elan toolchain list
lean (default)
lean-bootstrap

The lean toolchain is linked to my local stage1 build of lean4, and the lean-bootstrap toolchain is linked to my local stage0 build of lean4.

[lovettchris]

ok, great, thanks.