Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Apple switching to ARM


view this post on Zulip Email Gateway (Aug 23 2022 at 09:15):

From: Manuel Eberl <eberlm@in.tum.de>
Heads up: it seems that Apple just announced that they will be switching
some of their products from Intel x86_64 CPUs to ARM-based ones.

They said they will keep releasing Intel-based Macs as well, but I for
one (albeit just an outside observer) would suspect that this is just a
transition period and I would be surprised if their ultimate goal was
not to get away from Intel entirely.

I imagine this will be quite problematic for us if we want to keep
supporting macOS. Last I heard, Poly/ML only had an interpreter on ARM,
not a compiler, which comes with a big performance loss (correct me if I
am mistaken).

Apple provides an emulator for unported x86_64 applications on ARM, but
I doubt that that is sufficient for a demanding application like Isabelle.

Manuel

view this post on Zulip Email Gateway (Aug 23 2022 at 09:15):

From: Nick Spinale <nick@nickspinale.com>
Last fall, I built and ran Isabelle 2019 and all of its dependencies on Arm (aarch64-linux) using Nix [1].

Last I heard, Poly/ML only had an interpreter on ARM, not a compiler, which comes with a big performance loss.

I did encounter serious performance problems with Poly/ML. From what I can gather from the Poly/ML source, you are correct [2].

For reference, my code: https://github.com/nspin/nix-isabelle

[1] https://nixos.org/features.html
[2] https://github.com/polyml/polyml/blob/0ad5aa87ea7bd8eace41a180e2f5bad588c4635d/configure.ac#L433


Nick Spinale (nickspinale.com)


view this post on Zulip Email Gateway (Aug 23 2022 at 09:15):

From: Makarius <makarius@sketis.net>
What kind of hardware are you using for this?

Looking around a little bit, I've found the following:

* Linux laptop with 4 GB RAM from https://www.pine64.org/pinebook-pro (for $200)

* Virtual ARM / aarch64 systems for testing / porting open-source projects:
https://www.linaro.org

Makarius

view this post on Zulip Email Gateway (Aug 23 2022 at 09:15):

From: Nick Spinale <nick@nickspinale.com>
I was using a Samsung Chromebook Plus (XE513C24-K01US) with ChromeOS replaced with custom Linux.


Nick Spinale (nickspinale.com)



Last updated: Apr 25 2024 at 20:15 UTC