M1 MacOS

Stream: general

[Wouter Smeenk]

Hi, I am new to Lean and tried to install in on my M1 macbook. I followed: https://leanprover-community.github.io/install/macos.html which says to install x86 version. But I later discovered https://leanprover.github.io/lean4/doc/setup.html which says it is also available for M1 arch. How do I uninstall everything done in this first guide? I know how to uninstall elan using brew, but does this also remove the other steps I did with elan?

[Wouter Smeenk]

Ah it seems you can do elan toolchain uninstall stable Is this enough to remove everything?

[Sebastian Ullrich]

That should be sufficient, yes. You can also delete all of ~/.elan after uninstalling elan if you want to be sure

[Sebastian Ullrich]

@Scott Morrison That script seems to be a bit confused, stable isn't even Lean 4. And the M1 instructions really should be updated

[Scott Morrison]

Sorry, I didn't touch the M1 instructions at all, not having one. :-) Could we get a volunteer to write the M1 section at https://leanprover-community.github.io/install/macos.html?

[Scott Morrison]

If it is just a matter of replacing stable in the M1 instructions everywhere with leanprover/lean4:nightly, I can do that at least right away.