VScode extension install fails

Stream: lean4

[Shreyas Srinivas]

I setup a new ubuntu 24.04 machine. I thought this might be an opportunity to test out the vscode method of setup.

1. The extension claimed to have installed elan but it's clearly not added to the PATH variable.
2. When I ask vscode to setup a new lean project, I get "Unknown errors".

I have both git and curl installed and these are the prerequisites. The ~/.elan folder exists and I can see the toolchains.

So my best guess is that there was a silent failure at the step that elan is added to PATH, and this might be because of permissions. I have not debugged any further and am now on my way to fix things by hand.

[Shreyas Srinivas]

A short update: after fixing the path issue, it seems the extension doesn't open the project folder after setting it up. It just throws its hands up and says "Unknown error"