Installing Lean with Visual studio code "permission denied"

Stream: new members

[Jonathan Bekaert]

I am using the lean 4 setup guide in visual studio coda to install lean 4. I am at the step after I ran the code line

/bin/bash -c "$(curl -fsSL https://raw.githubusercontent.com/Homebrew/install/HEAD/install.sh)".

It said I needed to run two lines to add Homebrew to my path, but when entering the line:

(echo; echo 'eval "$(/opt/homebrew/bin/brew shellenv)"') >> /Users/jonathan/.bash_profile

I got bash: /Users/jonathan/.bash_profile: Permission denied

Can anyone help me? Because at the next step of instalilng the lean version manager it won't do it because it says:

error: could not write rcfile file: '/Users/jonathan/.bash_profile'
info: caused by: Permission denied (os error 13)

[Bulhwi Cha]

One of my mentees I'm teaching Lean also had this problem when trying to install it. I don't have a Mac, so I'm not sure why this happened.

[Julian Berman]

Welcome. Can you show us what ls -l ~/.bash_profile says for you?

[Jonathan Bekaert]

It replies:
-rw-r--r-- 1 root staff 447 Jun 2 2020 /Users/jonathan/.bash_profile

[Julian Berman]

You can run sudo chown jonathan:staff ~/.bash_profile which will fix the permissions on that file, and then run the /bin/bash -c "$(curl -fsSL https://raw.githubusercontent.com/Homebrew/install/HEAD/install.sh)" line again. Let me know what that does.

[Jonathan Bekaert]

It worked, thank you!

[Julian Berman]

Great!