Email Gateway (Oct 14 2026 at 20:55): Email Gateway (Oct 14 2026 at 20:55):From: Makarius <makarius@sketis.net>
This is a brief summary of the multi-platform situation in RC4, and thus
probably also for the final release.
- x86_64-linux: everything should work smoothly as before; this is de-facto
the main development and test platform of Isabelle.
- arm64-darwin: for the first time, everything should work without Intel
emulation (Rosetta 2); z3 on arm64-darwin is somewhat unstable when many
instances are run in parallel, but this situation has been the same for
x86_64-darwin in the past (e.g. seen in parallel builds of Isabelle/AFP).
- x86_64-darwin: still fully supported, for a few years to come; I have an
old Intel i3 MacMini on my desk for testing (a bit slow, but works fine).
- arm64-linux: a fringe platform that becomes gradually more important,
e.g. for containers on Apple Silicon or low-energy servers with ARM hardware;
notable omission: z3 --- it was found too unstable, often non-terminating,
unlike the version for arm64-darwin.
- x86_64-windows: slightly improved support, especially for the desktop app
launcher, including the 7zip SFX module; tangible support for Nonvisual Access
Technology (audio output or Braille display), based on a slightly patched
version of Java and its included Java Access Bridge. As before, a few
components add-on are absent on Windows, e.g. Mlton.
- arm64-windows: not available, no plans to support it (lack of test
hardware, lack of significance); better rely on MS doing the emulation of
x86_64-windows for us, but I don't have test hardware to check even that.
Implicitly, the idea behind all that: We deliver a regular application that
happens to work on all these platforms. We don't "containerize" user working
environments, with a private operating system for every compartment.
Ultimately, end-users should get "Isabelle" as some kind of meta-operating
system where almost everything just works, in reminiscence to ancient LISP
machines, before Unix became popular. This particularly means that
Isabelle/Scala needs to be used as the primary means for systems programming
of any kind (not funny scripting languages from distant past).
Makarius
Last updated: Oct 29 2026 at 04:52 UTC