Zulip Chat Archive

Stream: general

Topic: cp permission denied

Anna Brunkhorst (Sep 12 2022 at 13:43):

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 (Sep 12 2022 at 13:46):

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 (Sep 12 2022 at 14:09):

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.

Last updated: Aug 03 2023 at 10:10 UTC