Installation Issue (Mac)

Stream: new members

[Michael]

Hello, I am new to Lean and have tried to install it on my Macbook. When I tried /bin/bash -c "$(curl -fsSL https://raw.githubusercontent.com/leanprover-community/mathlib-tools/master/scripts/install_macos.sh)" && source ~/.profile, I got an error message so I instead tried to it step by step as detailed on https://leanprover-community.github.io/install/macos_details.html

When I tried to install elan in Terminal, it didn't work so I went to https://github.com/leanprover/elan/releases/tag/v1.0.6 to do it manually. However I don't think it worked because after successfully completing the other steps, my test file is not working in VS Code. I have attached screenshots of what it is showing in VS Code and the error message I get when trying to install using /bin/bash -c "$(curl -fsSL https://raw.githubusercontent.com/leanprover-community/mathlib-tools/master/scripts/install_macos.sh)" && source ~/.profile. Please could someone help me with this? Screenshot-2021-08-05-at-18.54.53.png Screenshot-2021-08-05-at-18.56.44.png

[Bryan Gin-ge Chen]

Is your MacBook running Apple Silicon by any chance? E.g. is it on this list? https://support.apple.com/en-us/HT211814

If so, maybe the steps in this thread might help: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/M1.20macs/near/227370426

[Julian Berman]

(deleted)