lean installation debugging

Stream: new members

[Servaas Clerckx]

Hello everyone, I'm completely new to the lean ecosystem and community. I have some trouble installing lean with VSCode and have (mostly) exhausted the online resources. How should I create a thread to debug my issue? Is that a stream?

[Riccardo Brasca]

This thread is perfectly fine. Can you describe your error?

[Servaas Clerckx]

Ah okay, perfect. My problem is that when I open the Main.lean file in the lean4-samples the infoview is stuck on "Waiting for Lean server to start...".

image.png

I followed this guide: https://www.youtube.com/watch?v=ZV6FLGTTzdc. (Note that I accidentally installed lean3 (lean extension on VSCode) first. I uninstalled that version and then executed the steps in the tutorial. )

The debugging steps I have tried:

1. Uninstall and reinstall lean4 extension
2. Uninstall and reinstall VSCode (not the extensions)
3. Set-ExecutionPolicy -ExecutionPolicy Unrestricted -Scope CurrentUser fix during install as described in [https://leanprover-community.github.io/archive/stream/270676-lean4/topic/VSCode.20.22Waiting.20for.20lean.20server.20to.20start.2E.2E.2E.22.html]

[Riccardo Brasca]

Have you installed elan and friends?

https://leanprover-community.github.io/get_started.html

[Servaas Clerckx]

I think so? This is my view from PowerShell.
image.png
I clicked the button "Install lean using elan" when prompted by the VSCode plugin.

[Riccardo Brasca]

And did you open a folder in VS Code rather than just a file?

[Servaas Clerckx]

Yes, I opened the lean4-samples folder which I cloned from the GitHub

[Sky Wilshaw]

I think you need to open the HelloWorld folder not its containing folder.

[Servaas Clerckx]

Oh wow that did it, thank you so much

[Riccardo Brasca]

Yes, you need to open that