VSCode "Waiting for lean server to start..."

Stream: lean4

[dudubao2007]

When I opened my VSCode yesterday, It just stuck here.
VSC.png
I've tried many methods, including restarting VSCode, restarting my PC, reloading VSCode extension for lean4, reinstalling lean4, but NONE worked.
What's weirder is that VSCode and lean worked well two days ago on both of my PCs, but now neither.
What should I do?
(Lean (version 4.0.0, commit d2dcff1f9a20, Release))

[Arthur Paulino]

Try opening VS Code in your project folder "foo" (not in the "lean" folder)

[dudubao2007]

It still doesn't work.

[Arthur Paulino]

can you send a screenshot?

[dudubao2007]

image.png

[dudubao2007]

2 days ago, opening a single file worked normally as well.

[Mauricio Collares]

What's the version of your Lean4 VS Code extension?

[Matthew Ballard]

Huh, I have this problem too but no issue with the lsp in the nvim extension.

[Matthew Ballard]

My extension version is 0.0.66 and my vs code version is 1.64.2. (Though this is not pressing for me since I have migrated to nvim for the time being.)

[dudubao2007]

extension version 0.0.66(but yesterday it's 0.0.65, it upgrades automatically).I guess if able to use the versions before, the problem can be fixed.

[Arthur Paulino]

On the extensions menu you can click on the gear and install other versions

[dudubao2007]

I switched to 0.0.63, and it is solved. :smiley:

[dudubao2007]

Where to report this bug?

[dudubao2007]

Many thanks to all of you :heart:

[Mauricio Collares]

Newer versions of the extension expect a lean-toolchain file inside the project root folder

[Mauricio Collares]

(containing a single line with a Lean version, such as leanprover/lean4:nightly-2022-02-11)

[dudubao2007]

Thank you! It works!

[Daniel Fabian]

how do we work around it for the compiler itself? I use the current master version and override the path in the extension to build output folder

[Mark Wilhelm]

Reverting to vs-code extension version 0.0.63 also fixed mine, thanks dudubao

[Mauricio Collares]

Given the above reports, maybe VS Code should fall back to the workspace root in case a lean-toolchain/leanpkg.toml file is not found (cc @Chris Lovett)

[Arthur Paulino]

Another possibility: explicitly say that such file wasn't found (and maybe list what was found instead so the user knows where it's looking). This may also mitigate those cases in which people open VS Code in wrong directories

[Nathaniel Yazdani]

I ran into this issue yesterday, too, and filed an issue: https://github.com/leanprover/vscode-lean4/issues/122. Would probably help debugging if others shared any potentially relevant observations of this bug :-)

[Gabriel Ebner]

I've put in a quick fix, so you should be able to use 0.0.67 again.

[Daniel Fabian]

i can confirm 0.67 works again for me.

[Chris Lovett]

Also, some regressions in handling of "ad-hoc" and "untitled" files are fixed in this PR:
https://github.com/leanprover/vscode-lean4/pull/127

[Will Wan]

0.0.71 fails as well, downgrading to 0.0.63 does solved my problem, thanks!

[Leonardo de Moura]

@Will Wan I had the same problem, but it went away after I updated VS Code.

[Damiano Testa]

I just tried installing Lean4, following the instructions here. I did not get the "Failed to start 'lean' language server" popup (I already have Lean3 installed) and I get the Waiting for Lean server to start... forever. I tried following the troubleshooting section of the install page and I get

$ lake init foo
error: toolchain 'stable' does not have the binary `/home/damiano/.elan/toolchains/stable/bin/lake`

Unfortunately, I do not understand most of what is being said in this topic to really comfortably say that what is said here does not solve my issues...

[Damiano Testa]

(I want to pre-emptively say that I apologize for the silly questions that I will ask: I feel quite helpless with most of what goes on with the more CS side of Lean. I'd be happy to help with maths questions in return for patient support with software help! :smile: )

[Damiano Testa]

Ok, this was easy: I had missed that there were more in-depth instructions! :face_palm:

I managed to install Lean4 and the lean server is running!

[Marc Huisinga]

Which instruction was missing for you on the quickstart page?

[Damiano Testa]

I was directed here from the github page and I did not realize that this was section 3 of many more. It was my incompetence, not the unavailability of information.

[James Gallicchio]

Hm, I'm now having this issue. VSCode version 1.67.1, extension version 0.0.72, and I've tried everything suggested at the aforementioned links D:

[James Gallicchio]

What's strange is that it works fine in another project directory. Yet lake buildworks fine in the new project, so I assume the new project is set up correctly?

[James Gallicchio]

Oh boy, it seems to be due to the presence of a dependency in my lakefile...

[James Gallicchio]

Ah, I wrote name := "..." instead of name := `.. which seems to be working again. No clue why these issues are connected.

[Wojciech Nawrocki]

It looks like when there is an error in lakefile.lean, the infoview just gets stuck showing "Waiting for lean server to start..." rather than display the error.

[James Gallicchio]

And now the string syntax is working fine... I'm quite confused -- what's most confusing is that an error in the lakefile should show up when doing lake build

[James Gallicchio]

but now I can't reproduce it. if it happens again I'll try to collect more information

[Wojciech Nawrocki]

Hm, so part of the problem seems to be that when lakefile.lean contains errors, lake serve prints them e.g. like so

./lakefile.lean:5:18: error: unknown constant 'Lake.PackageFacet.olean'
error: package configuration `./lakefile.lean` has errors

but then continues to execute the LSP server anyway. From the vscode extension's perspective, since it received no error code the server started up okay, and then this somehow leads to showing "Waiting" forever. Perhaps Lake should just exit with 1 at this point. /CC @Mac

[Mac]

@Wojciech Nawrocki this is actually a new feature, not a bug. See Lake #52. :stuck_out_tongue_wink:

[Wojciech Nawrocki]

I see! Then vscode-lean4 should detect and handle this case.

[Sebastian Ullrich]

Wojciech Nawrocki said:

Hm, so part of the problem seems to be that when lakefile.lean contains errors, lake serve prints them e.g. like so

On stdout? That seems like a bug to me, serve should only ever speak LSP on stdout.

[Gabriel Ebner]

I believe this is just https://github.com/leanprover/vscode-lean4/issues/90 The main issue here is that the lake errors are only returned as plain old diagnostics and not interactive diagnostics (i.e., atm you will only see the squiggle but nothing in the infoview).

[Sebastian Ullrich]

That may compound the issue, but it looks like at least some plain-text messages are printed to stdout (by runFrontend, I assume):

$ lake serve 2> /dev/null
./lakefile.lean:1:0: error: unknown package 'FLake'
./lakefile.lean:3:0: error: unknown namespace 'Lake'
./lakefile.lean:5:0: error: expected command

[Gabriel Ebner]

Apparently I've never noticed that because neovim's LSP implementation can recover from the noise on stdout.

[Sebastian Ullrich]

Huh, Emacs as well apparently

[Alistair Tucker]

I too have been having problems with the Quickstart instructions on Mac. It looks as if Damiano resolved his problems by moving on to 3.1 Extended Setup notes. Before I do that, I thought I'd make a quick note in this thread about my experience with the first page of section 3.

2. Launch VS Code and install the lean4 extension. Works fine

3. Create a new file using "File > New File" and click the Select a language link…
When I select File > New File from the menu, it requests a filename and gives me a choice of Text file or Jupyter Notebook. After that nothing at all. However if I select File > New Text File then I do indeed get a file buffer and a Select a language link.

…type in lean4 and hit ENTER. You should see the following popup…
I can type in lean4 and find the file type, but then no such popup appears. I get brief notifications in the bottom right saying things like:

info: latest update on nightly, lean version nightly-2022-05-18
 info: downloading component 'lean'
 Checking Lean setup…
 Checking Elan setup…

These last two disappear very quickly indeed.

And then it’s just
Waiting for Lean server to start...

Terminal has nothing going on, while using cmd-shift-p to run Developer: Reload Windowgives me more notifications like those above, but no useful change in state.

[Sebastian Ullrich]

Alistair Tucker said:

3. Create a new file using "File > New File" and click the Select a language link…
When I select File > New File from the menu, it requests a filename and gives me a choice of Text file or Jupyter Notebook. After that nothing at all. However if I select File > New Text File then I do indeed get a file buffer and a Select a language link.

Thanks, it looks like this is a recent VS Code change. I updated the docs accordingly. I can't reproduce the "Waiting for Lean server to start..." message on Linux however. Does the editor not do anything in that case, e.g. mark syntax errors in red?

[Sebastian Ullrich]

Alistair Tucker said:

…type in lean4 and hit ENTER. You should see the following popup…
I can type in lean4 and find the file type, but then no such popup appears

From the messages, it looks like you already had elan installed, perhaps from a previous try

[Alistair Tucker]

Thanks! You’re quite right, elan was already there. This is a new OS install but I copied my files across and elan came with them. So I've deleted it rm -rf ~/.elan and started again. This time things have gone more smoothly! At least #eval Lean.versionString works; now I can begin to play. I'm not sure it matters but there is still an error message in the output:

(base) iMac:~ ali$ bash -c 'curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain leanprover/lean4:nightly || echo && read -n 1 -s -r -p "Install failed, press ENTER to continue..."' && exit
info: downloading installer
info: syncing channel updates for 'nightly'
info: latest update on nightly, lean version nightly-2022-05-18
info: downloading component 'lean'
Total: 116.7 MiB Speed:   8.8 MiB/s
info: installing component 'lean'
info: default toolchain set to 'leanprover/lean4:nightly'

  leanprover/lean4:nightly installed - Lean (version 4.0.0-nightly-2022-05-18, commit eb170d1f43e8, Release)

Install failed, press ENTER to continue...

[Sebastian Ullrich]

Yes, I got the same message. You can ignore it. https://github.com/leanprover/vscode-lean4/pull/178

[Chandan Sah]

image.png
when I started working on Lean proof assistant on visual studio code, I have followed the instructions on this YouTube video https://www.youtube.com/watch?v=yZo6k48L0VY

but the lean Infoviewer didn't show any thing just "Waiting for Lean server to start..."

I tried switching the lean 4 version back to 0.0.63, still it is not solved.

Is there anyway to get everything solved?

[Chandan Sah]

image.png For your information, while installing "Lean using Elan", I got the following prompt which I felt is unusual

[Mac]

Well, that errors means that Elan (and thus Lean) failed to install. Apparently, this is because you cannot run scripts on your system. Do you know why that might be?

[Chandan Sah]

Mac said:

Well, that errors means that Elan (and thus Lean) failed to install. Apparently, this is because you cannot run scripts on your system. Do you know why that might be?

Noo
The red text says:
File C:\Users\hp\Desktop\LEAN\lean4-samples\elan-init.ps1 cannot be loaded because running scripts is
disabled on this system. For more information, see about_Execution_Policies at https:/go.microsoft.com/fwlink/?LinkID=135170.
At line:1 char:7

• $rc = .\elan-init.ps1 -NoPrompt 1 -DefaultToolchain leanprover/lean4: ...
• ~~~~~~~~~~~~~~~
  + CategoryInfo : SecurityError: (:) [], PSSecurityException
  + FullyQualifiedErrorId : UnauthorizedAccess

[Chandan Sah]

image.png

[Chandan Sah]

image.png

[Chandan Sah]

Given these are highlighted instructions, what commands should I enter?

[Sebastian Ullrich]

I believe a students of ours fixed this by running, in a new PowerShell window,

Set-ExecutionPolicy -ExecutionPolicy Unrestricted -Scope CurrentUser

You may set it back to Restricted after the installation
/cc @Chris Lovett

[Chandan Sah]

2022-07-09-15-24-10.mkv

[Chandan Sah]

I followed your steps, it dint work first, Then I restarted vs code and retried now it's working perfectly.

@Sebastian Ullrich

Could you Please tell How to set it to restricted again?

[Sebastian Ullrich]

Set-ExecutionPolicy -ExecutionPolicy Restricted -Scope CurrentUser

I think

[Chandan Sah]

Thank you

[Chris Lovett]

I filed a new issue to track this PowerShell complication here: https://github.com/leanprover/vscode-lean4/issues/216

[Chris Lovett]

Here's the fix which also contains an important fix that was causing "waiting for lean server to start..."
https://github.com/leanprover/vscode-lean4/pull/217

[Chris Lovett]

This fix is now merged so this issue should now be resolved in version 0.0.83 of the vscode extension.

[Dominique Danco]

I'm running into the same problem today with v0.0.95 of the extension -- anyone know how to fix this?

[Dominique Danco]

I've also tried switching to 0.0.83, and same issue

[Chris Lovett]

The thread morphed a bit, can you paste the specific error, screen shot and info about which OS platform you are using, and what state you were in before it started, like clean machine, no elan, or elan was already installed, and so on, thanks. Also which lean repo are you editing, so I can see what the lean-toolchain and lakefile.lean contains?

[Dominique Danco]

image.png Here's the screenshot; I'm getting no error messages, just the server never starting. I'm on macOS Big Sur 11.6.6, I downloaded elan a while ago (can't remember exactly how) and updated yesterday with brew upgrade elan, then did lake build

[Dominique Danco]

the repo is private (I can add you if necessary), but the lean-toolchain is as follows:
leanprover/lean4:nightly-2022-09-20

and here is a screenshot of the lakefile.lean image.png

everything was working properly with this same code on a different laptop, but I just switched computers. thanks for the help!

[Jannis Limperg]

So lake build works but the extension doesn't?

[Dominique Danco]

yep

[Jannis Limperg]

That's very strange. Perhaps try to nuke and reinstall VSCode and the extension. (I don't use VSCode, so others will likely have more constructive suggestions.)

[Jannis Limperg]

I tried to reproduce, but when I open Project/FreshNames.lean (at commit 5a1a8dc5 ) in Emacs or VSCode, everything seems to be working fine.

[Dominique Danco]

I'll try reinstalling VSCode and see what happens

[Dominique Danco]

well, that worked :shrug: silly VSCode. all good now

[Jannis Limperg]

Nice!

[Chris Lovett]

If it happens again, it can also be handy to get the contents of the "Lean: Editor" Output page:
image.png