Installation trouble

Stream: new members

[Jackie Lang]

I am trying to install Lean4 on my Mac. I ran the command in the terminal, but I don't know if it was successful. I went ahead and tried to "install" the Mathematics in Lean book. When I type either source ~/.profile or source ~/.bash_profile I get the following message: no such file or directory: /Users/jaclynlang/.profile. I did install Mathematics in Lean and I have a folder called mathematics_in_lean. But when I run the command lake exe cache get, I get the message: zsh: command not found: lake. Can someone help me figure out what is going on? Thank you!

[A.]

What happens if you try to follow these instructions?

[Jackie Lang]

Thanks for the suggestion. It seems things are working now. I'll ask again if something goes wrong.