cp permission denied

Stream: general

[Anna Brunkhorst]

Hello all! I'm a student trying to follow the directions to install Lean on Windows 11 and am on the Python steps. I've installed Python, and when i run which python I get /c/Python310/python. When I try to run cp "$(which python)" "$(which python)"3, I get cp: cannot create regular file '/c/Python310/python3.exe': Permission denied. I'm very new to terminal & these types of commands; what went wrong where? Is it because Python installed outside of my user directory, or is that irrelevant?

[Ruben Van de Velde]

Yeah, you're in this branch of the instructions:

If it is any other directory, you might have an existing version of Python. Ask for help in the Zulip chat room (linked above).

I'm guessing someone who knows about Windows will be along soon

[Anna Brunkhorst]

Seems Python just installed to the wrong directory the first time! Wasn't paying enough attention and skipped the customization step. Reinstalled and the command now works.