stuck installing lean4

Stream: lean4

[Wouter van Doorn]

Hello! I tried https://leanprover-community.github.io/install/windows.html but I keep seeing "Waiting for Lean server to start..."
Can anyone help me out?

[Patrick Massot]

I'm afraid this isn't enough information to help you. What are you trying to do with Lean? Did you get some project to open? Did you create one?

[Kevin Buzzard]

Did you open the root directory of a correctly-formatted Lean project using VS Code's "open folder" functionality? Can you send a screenshot of your VS Code with the file manager open? Here's an example of what it would be nice to see -- especially if we could also see the error.

example.png

[Wouter van Doorn]

This is what it looks like on my end currently:
image.png

[Patrick Massot]

From your screenshot, it looks like you opened a folder containing several Lean projects, but you need to open one of those projects.

[Patrick Massot]

In your case you want to open the HelloWorld folder.

[Wouter van Doorn]

Thanks to both of you!!

[Patrick Massot]

@Wojciech Nawrocki it would be really nice to improve the VSCode extension message. Steps to reproduce:

• Create folder /tmp/not_a_project
• Create file /tmp/not_a_project/test.lean containing Lean code, say #check Nat
• Open folder /tmp/not_a_project in VSCode

The infoview opens and says "Waiting for Lean server to start..." forever. The simplest improvement would be to add a paragraph starting with "If this messages stays for more than 20 seconds then you may want to..."

[Wojciech Nawrocki]

I would say the proper fix would be to implement multi-folder workspaces (see vscode-lean4#138) analogously to what the Rust extension does, for example. Perhaps @Marc Huisinga is interested :)

[Wojciech Nawrocki]

That issue is specifically about the fact that lean4-samples does not work when opened as a top-level folder in VSCode.

[Marc Huisinga]

Wojciech Nawrocki said:

I would say the proper fix would be to implement multi-folder workspaces (see vscode-lean4#138) analogously to what the Rust extension does, for example. Perhaps Marc Huisinga is interested :)

It's on my to-do list :)

[Patrick Massot]

I still think a better message would be useful while waiting for a proper fix.

[Marc Huisinga]

Patrick Massot said:

I still think a better message would be useful while waiting for a proper fix.

Could you create an issue for this?
Adding other errors related to the VSCode extension that frequently confuse newcomers would also be very helpful.

[Patrick Massot]

https://github.com/leanprover/vscode-lean4/issues/323

[Marc Huisinga]

Thanks! :)