Alcides Fonseca

40.197958, -8.408312

Installing Lean4 on the M1 architecture

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 -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.