Email Gateway (Jan 23 2026 at 21:49): Email Gateway (Jan 23 2026 at 21:49):From: Makarius <makarius@sketis.net>
Since macOS 26 is the last version that supports the old Intel platform via
emulation, we need to reconsider our traditional approach to the macOS
platform, where the Isabelle distribution (and ".app") was "hybrid" for Intel
and ARM. Thus the same download worked on both platforms, but on ARM it
required Rosetta 2, which is going to disappear after macOS 26.
Concerning Intel, I have now invested 360 EUR into a refurbished Mac Mini 2018
(i3 with 4 cores, 16 GB RAM, 1 TB SSD). The 2018 line is the last one using
Intel CPUs, it supports macOS 12, 13, 14, 15, but not macOS 26. See also
https://everymac.com/systems/apple/mac_mini/specs/mac-mini-core-i3-3.6-late-2018-specs.html
for details.
Thus we can easily continue x86_64-darwin for Isabelle contrib executables, as
long as we have macOS 12..15 as our active baseline. There are many years
ahead, until the upper end macOS 15 will have to be discontinued. Only
afterwards, our support for macOS will be for ARM exclusively. Note that I
will soon discontinue macOS 12 and move to macOS 13, because it helps to
provide uniform VSCodium and GHC/stack executables.
Concerning pure arm64-darwin support, there is still a lot of homework to do
concerning external provers and solvers. When that is done, we can split the
Isabelle application bundle into x86_64-darwin vs. arm64-darwin. That will
mark the beginning of the "macos" vs. "macos_arm" era, following the "linux"
vs. "linux_arm" from some years ago. (It will be many more years, until
windows_arm might become relevant.)
I would like to see macos_arm already for Isabelle2026 (October 2026), but it
is probably more realistic for a subsequent Isabelle release in 2027. Note
that when macOS 27 hits the end-user market, people can no longer run Isabelle
with all its add-on tools.
Makarius
Email Gateway (Jan 24 2026 at 12:06):From: Lawrence Paulson via isabelle-dev <isabelle-dev@mailman.proof.cit.tum.de>
On 23 Jan 2026, at 21:48, Makarius <makarius@sketis.net> wrote:
Thus we can easily continue x86_64-darwin for Isabelle contrib executables,
Might be worth asking how many people still need this.
Note that when macOS 27 hits the end-user market, people can no longer run Isabelle with all its add-on tools.
What’s this?
Larry
Email Gateway (Jan 24 2026 at 12:07):From: Makarius <makarius@sketis.net>
On 24/01/2026 13:06, Lawrence Paulson wrote:
Note that when macOS 27 hits the end-user market, people can no longer run Isabelle with all its add-on tools.
What’s this?
It is the next macOS release after current macOS 26. I don't know anything
about its planned timeline, though.
Makarius
Email Gateway (Jan 24 2026 at 13:11):From: Makarius <makarius@sketis.net>
On 24/01/2026 14:00, Lawrence Paulson wrote:
I mean what’s this "people can no longer run Isabelle with all its add-on tools”?
So far, the Isabelle.app launcher insisted in Intel, to prompt for
installation of Rosetta 2. This will fail after macOS 26, and users need to
use Isabelle.app/isabelle/bin/isabelle jedit on the command-line.
I can change that easily, and make the launcher hybrid on Intel or ARM.
Afterwards, there will be some add-on tools that still insist on Intel: we
need to sort that out, maybe this year or next year.
Makarius
Email Gateway (Jan 24 2026 at 13:15):From: Lawrence Paulson via isabelle-dev <isabelle-dev@mailman.proof.cit.tum.de>
Oh that. I wonder if anybody uses the app? As it stands, it is very basic. It needs at least a drag and drop capability. It should not be difficult, but we need to find somebody who knows how to build these things.
Larry
On 24 Jan 2026, at 13:11, Makarius <makarius@sketis.net> wrote:
So far, the Isabelle.app launcher insisted in Intel, to prompt for installation of Rosetta 2. This will fail after macOS 26, and users need to use Isabelle.app/isabelle/bin/isabelle jedit on the command-line.
I can change that easily, and make the launcher hybrid on Intel or ARM. Afterwards, there will be some add-on tools that still insist on Intel: we need to sort that out, maybe this year or next year.
Email Gateway (Jan 24 2026 at 15:02):From: Makarius <makarius@sketis.net>
On 24/01/2026 14:15, Lawrence Paulson wrote:
Oh that. I wonder if anybody uses the app? As it stands, it is very basic. It needs at least a drag and drop capability. It should not be difficult, but we need to find somebody who knows how to build these things.
My guess is that most first-time Isabelle users on macOS use the desktop app,
because they don't know anything else.
Concerning drag-and-drop, it should be possible to find open-source examples
out there and imitate them. I've always ignored drag-and-drop in particular,
because it reminds me on super-retro desktop interaction from the late 1980s
or early 1990s.
Makarius
Email Gateway (Jan 24 2026 at 15:51):From: Lawrence Paulson via isabelle-dev <isabelle-dev@mailman.proof.cit.tum.de>
I can't think of a better way to open a particular theory that may be sitting in a deeply nested directory.
On 24 Jan 2026, at 15:02, Makarius <makarius@sketis.net> wrote:
Concerning drag-and-drop, it should be possible to find open-source examples out there and imitate them. I've always ignored drag-and-drop in particular, because it reminds me on super-retro desktop interaction from the late 1980s or early 1990s.
Last updated: Feb 04 2026 at 02:22 UTC