Zulip Chat Archive

Stream: new members

Topic: installing python


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

view this post on Zulip Thomas Browning (May 29 2020 at 21:29):

what does which python say?

view this post on Zulip Rose Lopez (May 29 2020 at 21:31):

what do you mean?

view this post on Zulip Patrick Lutz (May 29 2020 at 21:32):

If you type which python in the terminal, what's the output?

view this post on Zulip Thomas Browning (May 29 2020 at 21:32):

in the git bash, not the terminal, right?

view this post on Zulip Dan Stanescu (May 29 2020 at 21:32):

At the git bash prompt you may need to type ./python-3.8.3.exe

view this post on Zulip Dan Stanescu (May 29 2020 at 21:33):

Or maybe ./python-3.8.3

view this post on Zulip Dan Stanescu (May 29 2020 at 21:34):

If the .exe is in your current directory, that is.

view this post on Zulip Rose Lopez (May 29 2020 at 21:34):

yeah i was using git bash

view this post on Zulip Rose Lopez (May 29 2020 at 21:34):

it said /c/Users?Rose/AppData?Local?Microsoft?WindowsApps/python

view this post on Zulip Rose Lopez (May 29 2020 at 21:35):

after typing which python

view this post on Zulip Dan Stanescu (May 29 2020 at 21:35):

Oh, OK. So it is in your path.

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

view this post on Zulip Dan Stanescu (May 29 2020 at 21:36):

You should only need to type python

view this post on Zulip Rose Lopez (May 29 2020 at 21:37):

i was using that instruction page. I can try watching the video

view this post on Zulip Dan Stanescu (May 29 2020 at 21:37):

What happens if you type python at the prompt?

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

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

view this post on Zulip Rose Lopez (May 29 2020 at 21:40):

The video tutorial is private on you tube

view this post on Zulip Rose Lopez (May 29 2020 at 21:41):

sudo python returns command not found

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

view this post on Zulip Dan Stanescu (May 29 2020 at 21:44):

You can try to start typing then press Tab to complete the path.

view this post on Zulip Dan Stanescu (May 29 2020 at 21:45):

But first make sure it finds sudo : type which sudo or whereis sudo.

view this post on Zulip Dan Stanescu (May 29 2020 at 21:48):

I take that back. Git bash doesn't come with sudo.

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

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

view this post on Zulip Dan Stanescu (May 29 2020 at 21:57):

A power shell is a terminal that you run with admin privileges.

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

view this post on Zulip Rose Lopez (May 29 2020 at 22:01):

Thank you for your help! I will check out the link.

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

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

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Issue.20with.20git.20bash.20and.20python.20on.20Windows.2010/near/199222233


Last updated: May 14 2021 at 13:24 UTC