M1 Mac running Ubuntu VM

Stream: general

[Hector Padilla]

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]

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]

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]

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]

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

[Matthew Ballard]

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