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
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)
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
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: Nov 21 2024 at 12:39 UTC