Zulip Chat Archive

Stream: new members

Topic: Help with lean install (windows)


view this post on Zulip 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!

view this post on Zulip Kevin Buzzard (Dec 17 2019 at 22:33):

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

view this post on Zulip ZainAK283 (Dec 17 2019 at 22:36):

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

view this post on Zulip Kevin Buzzard (Dec 17 2019 at 22:37):

That's good

view this post on Zulip Kevin Buzzard (Dec 17 2019 at 22:37):

that means it's doing something

view this post on Zulip Kevin Buzzard (Dec 17 2019 at 22:37):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Dec 17 2019 at 22:39):

that looks good

view this post on Zulip Kevin Buzzard (Dec 17 2019 at 22:39):

maybe you're good to go

view this post on Zulip ZainAK283 (Dec 17 2019 at 22:41):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Dec 17 2019 at 23:11):

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

view this post on Zulip Kevin Buzzard (Dec 17 2019 at 23:12):

Are you using git bash?

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Dec 17 2019 at 23:13):

You got "command not found"

view this post on Zulip 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.

view this post on Zulip 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: May 12 2021 at 04:19 UTC