I upgraded to a new M1Max MacbookPro (will have to review it next), and I had to install lean4 today. Unfortunately, elan does not work in the M1 architecture as expected, so I had to use rosetta. here’s how I set it up:
1. Install VSCode: brew install --cask visual-studio-code && code --install-extension jroesch.lean
2. Install Rosetta2 /usr/sbin/softwareupdate --install-rosetta --agree-to-license
3. Install elan manually: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | arch -x86_64 sh
4. Install latest lean: elan default leanprover/lean4:nightly
5. Configure the lean path in the lean4 vs code extension to point to this lean: “Lean4: Executable Path” to arch -x86_64 lean
It will work. Now let’s hope that elan adds supports for arm64 binary fetching.