Zulip Chat Archive

Stream: new members

Topic: Help with lean install (windows)

ZainAK283 (Dec 17 2019 at 22:31):

I'm trying to follow https://www.youtube.com/watch?v=2f_9Zetekd8
I get to about the 3:30 mark, where it says "Lean installed, press enter to continue", but get:

"Unable to start the Lean server process: Error: spawn lean ENOENT --- The lean.executablePath "lean" may be incorrect, make sure it is a valid Lean executable"

Help is very much appreciated!

Kevin Buzzard (Dec 17 2019 at 22:33):

If you open a terminal in VS Code and type lean, does it find Lean?

ZainAK283 (Dec 17 2019 at 22:36):

Annotation-2019-12-17-223622.jpg
Looks like it does nothing

Kevin Buzzard (Dec 17 2019 at 22:37):

That's good

Kevin Buzzard (Dec 17 2019 at 22:37):

that means it's doing something

Kevin Buzzard (Dec 17 2019 at 22:37):

but is that exactly the same terminal that VS Code is using?

ZainAK283 (Dec 17 2019 at 22:39):

I believe so, I'm not really familiar with terminals or VS Code
Bottom-left corner says "Lean [tick]: (checking visible files)" if that means something

Kevin Buzzard (Dec 17 2019 at 22:39):

that looks good

Kevin Buzzard (Dec 17 2019 at 22:39):

maybe you're good to go

ZainAK283 (Dec 17 2019 at 22:41):

Looks like I am!
#eval 1+1
Displays 2
Thank you!

ZainAK283 (Dec 17 2019 at 23:09):

I'm trying to install Mathlib as per https://github.com/leanprover-community/mathlib/blob/master/docs/install/windows.md
I've downloaded Python, gone into Git Bash, searched "which python", and get this result:
Annotation-2019-12-17-230556.jpg
I've turned off "App Installer python.exe" and "App Installer python3.exe" as it suggests further down

Kevin Buzzard (Dec 17 2019 at 23:11):

Did you start at the beginning of the link and follow the instructions exactly?

Kevin Buzzard (Dec 17 2019 at 23:12):

Are you using git bash?

Kevin Buzzard (Dec 17 2019 at 23:13):

The App Installer stuff is if you find the wrong python. Your problem is that you can't find any python at all.

Kevin Buzzard (Dec 17 2019 at 23:13):

You got "command not found"

Kevin Buzzard (Dec 17 2019 at 23:14):

Do you happen to know which directory the correct python is in? You should add that directory to your path.

ZainAK283 (Dec 17 2019 at 23:56):

Apologies - I hadn't checked "Add Python 3.x to PATH" which messed everything up
I've successfully installed Mathlib, created a new Lean project, and downloaded the tutorials
Thank you very much!

Last updated: Dec 20 2023 at 11:08 UTC