Zulip Chat Archive

Stream: general

Topic: M1 Mac running Ubuntu VM


Hector Padilla (Sep 10 2021 at 16:26):

I am trying to run this command and I am getting this error

curl: (22) The requested URL returned error: 404
elan: command failed: curl -sSfL https://github.com/leanprover/elan/releases/download/v1.0.7/elan-aarch64-unknown-linux-gnu.tar.gz -o /tmp/tmp.8TwPVfHKPp/elan-init.tar.gz

Does anyone know how to fix this?

Johan Commelin (Sep 10 2021 at 17:00):

I don't have a mac, but does this topic help? https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/M1.20macs

Matthew Ballard (Sep 10 2021 at 17:32):

The machine is being identified as arm-based linux and there is no elan build for such a combination. I encountered this with a 64 bit rpi4 and had to build from source.

Jason Rute (Sep 10 2021 at 18:57):

That makes sense. While M1 macs can simulate x86 via Rosetta, I don’t think containers (e.g. Docker containers) or virtual machines on M1 macs can use x86.

Hector Padilla (Sep 10 2021 at 19:22):

@Matthew Ballard How do you build from source. Sorry I am not familiar with that.

Matthew Ballard (Sep 10 2021 at 19:51):

This was for Lean4. It looks like the Lean3 instructions are similar.


Last updated: Dec 20 2023 at 11:08 UTC