Zulip Chat Archive
Stream: new members
Topic: installing python
Rose Lopez (May 29 2020 at 21:26):
I had some troubling getting python. I was able to successfully download, but after typing python-3.8.3.exe in the git bash terminal, I got a message, command not found. I am using Windows.
Thomas Browning (May 29 2020 at 21:29):
what does which python say?
Rose Lopez (May 29 2020 at 21:31):
what do you mean?
Patrick Lutz (May 29 2020 at 21:32):
If you type which python in the terminal, what's the output?
Thomas Browning (May 29 2020 at 21:32):
in the git bash, not the terminal, right?
Dan Stanescu (May 29 2020 at 21:32):
At the git bash prompt you may need to type ./python-3.8.3.exe
Dan Stanescu (May 29 2020 at 21:33):
Or maybe ./python-3.8.3
Dan Stanescu (May 29 2020 at 21:34):
If the .exe is in your current directory, that is.
Rose Lopez (May 29 2020 at 21:34):
yeah i was using git bash
Rose Lopez (May 29 2020 at 21:34):
it said /c/Users?Rose/AppData?Local?Microsoft?WindowsApps/python
Rose Lopez (May 29 2020 at 21:35):
after typing which python
Dan Stanescu (May 29 2020 at 21:35):
Oh, OK. So it is in your path.
Thomas Browning (May 29 2020 at 21:35):
The installation page (https://leanprover-community.github.io/install/windows.html) has instruction in this case. Did you try them?
Dan Stanescu (May 29 2020 at 21:36):
You should only need to type python
Rose Lopez (May 29 2020 at 21:37):
i was using that instruction page. I can try watching the video
Dan Stanescu (May 29 2020 at 21:37):
What happens if you type python at the prompt?
Rose Lopez (May 29 2020 at 21:38):
When I type python into git bash it said permission denied after /c/Users/Rose/AppData?Local?Microsoft?WindowsApps/python
Dan Stanescu (May 29 2020 at 21:40):
Right. You probably installed it with the wrong permission levels, although apparently it is in your directory. You could have used the --user option I guess.
Can you try sudo python at the prompt?
Rose Lopez (May 29 2020 at 21:40):
The video tutorial is private on you tube
Rose Lopez (May 29 2020 at 21:41):
sudo python returns command not found
Dan Stanescu (May 29 2020 at 21:43):
You need to give it the whole path then. We can fix that later, but now try to copy the path that which python spits out:
/c/Users/Rose/AppData?Local?Microsoft?WindowsApps/python
and do sudo /c/Users/Rose/AppData?Local?Microsoft?WindowsApps/python
This is a lot of pain on Windows.
Dan Stanescu (May 29 2020 at 21:44):
You can try to start typing then press Tab to complete the path.
Dan Stanescu (May 29 2020 at 21:45):
But first make sure it finds sudo : type which sudo or whereis sudo.
Dan Stanescu (May 29 2020 at 21:48):
I take that back. Git bash doesn't come with sudo.
Dan Stanescu (May 29 2020 at 21:52):
My best guess is you need a Windows power shell (Administrator) or make a user-owned python installation then.
Rose Lopez (May 29 2020 at 21:54):
After trying this step, "There should be two entries App Installer python.exe and App Installer python3.exe. Ensure that both of these are set to Off."
I get the message no python in ...(files). What is a Windows power shell or a user-owned python installation?
Dan Stanescu (May 29 2020 at 21:57):
A power shell is a terminal that you run with admin privileges.
Dan Stanescu (May 29 2020 at 21:59):
Maybe there is an easier solution to your problem. Maybe someone here has seen something similar recently and can hopefully chip in.
But for what it's worth here is this link:
https://stackoverflow.com/questions/56974927/permission-denied-trying-to-run-python-on-windows-10
Rose Lopez (May 29 2020 at 22:01):
Thank you for your help! I will check out the link.
Bryan Gin-ge Chen (May 29 2020 at 22:01):
The video tutorial is out of date so it was made private. I'll update the website.
Dan Stanescu (May 29 2020 at 22:58):
@Rose Lopez Rose, while Anaconda might be more than you need, it provides a very robust way to install Python.
Last updated: Dec 20 2023 at 11:08 UTC