Existing Python

Stream: general

[Josh Dornfeld]

Hello. I have an existing python program so when I run
"which python"
it says
"/c/Program Files/Python36/python"
and when I try to run
"$ cp "$(which python)" "$(which python)"3"
it returns
"cp: cannot create regular file '/c/Program Files/Python36/python3.exe': Permission denied"
Honestly, I have no idea what I'm doing. I'm downloading this for a class and following the community instructions led me here. Any help?

[Yakov Pechersky]

You're instructed to copy python to python3 because the lean executables expect to find a python3 in the PATH.

[Yakov Pechersky]

What command environment are you in? What's your terminal? You could always open the C:\Program Files\Python36\ folder in Windows Explorer and do the copying and renaming using the GUI.

[Josh Dornfeld]

I'm running Git Bash on Windows

[Yakov Pechersky]

Try running the Git Bash as an administrator. For example, search for Git Bash in your windows Start Menu search, right click, select Run as Administrator. Then the cp "$(which python)" "$(which python)"3 command should work.

[Josh Dornfeld]

I have Python downloaded from last year but my Professor instructed us to redownload Python to ensure that the set up is done correctly. I think that Git is pulling my existing Python program from my computer instead of the Python I just downloaded. How do I change that?

[Yakov Pechersky]

which is the command that identifies where a particular executable file lives. In Windows (and other Operating Systems), there is the concept of a PATH so that you have access to various files without having to know exactly where they are.

[Yakov Pechersky]

Have you ever edited the PATH before?

[Josh Dornfeld]

no

[Josh Dornfeld]

I appreciate your help by the way, thank you

[Yakov Pechersky]

When you installed Python again, was there a checkbox to add Python to PATH?

[Yakov Pechersky]

Like in the instructions on the Lean community website: Check Add Python 3.x to PATH.

[Josh Dornfeld]

yes. I clicked the box to add it to the PATH

[Yakov Pechersky]

Have you restarted your computer since that new Python installation?

[Josh Dornfeld]

I have not

[Yakov Pechersky]

That might help. What's going on here is that PATH is a list of folders that programs use to find those executables that I was talking about.

[Josh Dornfeld]

I'll give it a try!

[Yakov Pechersky]

When you write python, it first checks the first folder in the list -- "does it have anything called python in it"? If not, check the next folder, etc.

[Yakov Pechersky]

PATH is an "environmental variable" in your computer.

[Yakov Pechersky]

So all programs have access to it. The installation should have edited that variable and put the new folder it installed at the front of the list. Restarting your computer might help in that it will get all the other programs to recognize and use this new list.

[Yakov Pechersky]

We can always edit it ourselves. But first let's try the simpler, no editing solution, if that's alright with you.

[Josh Dornfeld]

when I run
"$ python3 --version"
it returns
"Python 3.6.4".
Which is my old version of Python. I just downloaded 3.8.5

[Yakov Pechersky]

To edit the path, here's what I do on Windows 10:

Search for `environment` in the Start menu Search
Select "Edit the system environment variables"
In the newly popped-up System Properties window, click on Environment Variables near the bottom right
In the newly popped-up Environment Variable window, under User Variables for ..., select Path
Click Edit

In my PATH, the first item is C:\Users\Yakov\.elan\bin, which are the lean utilities you'll need to run Lean.
The third item is C:\Users\Yakov\AppData\Local\Programs\Python\Python38-32\, which is a Python 3 installation.

[Yakov Pechersky]

I'm pretty sure that Python 3.6 will be good enough for using lean and the associated tools. But the instructions I just posted are the ones to check what's in your PATH

[Josh Dornfeld]

Yakov.jpg

[Josh Dornfeld]

That is what mine looks like

[Josh Dornfeld]

I forgot to blur out the user ahaha but oh well

[Yakov Pechersky]

Then I would do

rm "$(which python3)";
cp c:/Users/dornf/AppData/Local/Programs/Python/Python38/python c:/Users/dornf/AppData/Local/Programs/Python/Python38/python3;

[Yakov Pechersky]

which removes the new python3 you created in your last cp attempt (the one you did after Run as Administrator), and copy the Python 3.8 python to python3 using the paths directly, without relying on which. Then the only python3 accessible via your PATH will be the one in the AppData/.../ folder, which is the one you just installed.

[Josh Dornfeld]

Something else I just noticed - in the PATH it references Python38 but within my Program Files, the file is Python36

[Josh Dornfeld]

I tried running your command but python3 --version still returns
Python 3.6.4

[Josh Dornfeld]

oh wait, it worked!

[Josh Dornfeld]

Thank you so much Yakov

[Josh Dornfeld]

one more issue - running
pip3 --version
returns
pip 9.0.1 from c:\program files\python36\lib\site-packages (python 3.6)
I believe it should be 3.8 instead of 3.6, no?

[Yakov Pechersky]

You can do "which pip3" similarly.

[Yakov Pechersky]

Do you know what changed between the 3.6 and your message that it worked?

[Josh Dornfeld]

I was still entering the command
"cp "$(which python)" "$(which python)"3."
without realizing that it makes the code you sent me essentially useless

[Josh Dornfeld]

sorry, how do I fix the pip3 issue?

[Yakov Pechersky]

What's the output of which pip? How about which pip3?

[Josh Dornfeld]

which pip
returns
/c/Program Files/Python36/Scripts/pip

which pip3
returns
/c/Program Files/Python36/Scripts/pip3

[Yakov Pechersky]

Would you feel comfortable removing C:\Program FIles\Python36\Scripts from your PATH?

[Josh Dornfeld]

yes

[Yakov Pechersky]

So I'd test what happens when you delete that directory from the PATH, and try a new Git Bash and see what which pip3 gives you.

[Josh Dornfeld]

still the same output

[Yakov Pechersky]

Again, a restart might help. There's no way for something to know about pip3 at that location unless it's in the PATH

[Patrick Massot]

Josh Dornfeldsaid:

Honestly, I have no idea what I'm doing. I'm downloading this for a class and following the community instructions led me here. Any help?

And this is why I created bundled Lean+mathlib+VSCode for teaching...

[Julian Berman]

Josh Dornfeld said:

still the same output

Generally, it's good to avoid writing pip .... (For very similar reasons as what you're experiencing)

[Julian Berman]

Does what you're trying work if you instead write python3.8 -m pip ...?

[Julian Berman]

If so, it's good to prefer explicitly invoking pip with the Python version you mean to use.

[Josh Dornfeld]

unfortunately, the command
python3.8 -m pip ...
is not working either. It returns
bash: python3.8: command not found

I'm in the part of the community set-up instructions where it says,
"Test whether everything is working by typing python3 --version and pip3 --version. If both commands give a short output and no error, everything is set up correctly."

python3 --version is working, as it returns
"Python 3.8.5"
However, pip3 --version still returns
"pip 9.0.1 from c:\program files\python36\lib\site-packages (python 3.6)"
so from my understanding the pip3 PATH is still going towards my old installation of Python, and not my new installation of Python 3.8.

[Alex Peattie]

In your case @Josh Dornfeld if python3 --version works, you can use python3 -m pip in place of pip :smile:

[Josh Dornfeld]

Thank you @Alex Peattie that works! Is there a way to make it so pip or pip3 actually calls the code you wrote? I would imagine it will be easier in the future as to not have to remember "python3 -m pip"

[Alex Peattie]

You can always add aliases for long commands you use often:

http://jrcodeodyssey.com/bash/windows/2019/07/17/custom-bash-commands.html

Although if it's for using Lean, you'll really only have to use python3 -m pip install once (to install mathlibtools)

[Bryan Gin-ge Chen]

(It may also have to be run again if mathlibtools is updated.)

[Josh Dornfeld]

I believe everything is set up correctly. Thanks for the help everyone!