Email Gateway (Aug 17 2026 at 21:05): Email Gateway (Aug 17 2026 at 21:05):From: Makarius <makarius@sketis.net>
On 17/08/2026 22:21, Makarius wrote:
Note that there have been significant changes for the desktop application
launcher, both on macOS and Windows. Also note that macOS is now separate for
Apple Silicon (ARM) versus Intel.
More notes concerning macOS ARM vs. Intel.
Some months ago, I was under the impression that macOS 26 was the last version
with Rosetta 2, for emulation of Intel on Apple Silicon (ARM) hardware, and
that starting with "27" it will be discontinued --- meaning the macOS 27
release at the end of 2026.
Thus I made every effort to deliver a Isabelle2026 release that has
arm64-darwin executables for everything, with the notable exclusion of z3 ---
it needs further treatment in the near future.
I was wrong about the meaning of "27", because it will be macOS 28 in 2027,
not macOS 27 in 2026. Apple grants one more release cycle for Intel-emulation:
https://support.apple.com/en-us/102527
"""
Rosetta is currently available for any Mac with Apple silicon, and it will
remain available through the forthcoming macOS 27 — the next major macOS
release. Starting with computers using macOS 28, Rosetta functionality will be
available only for certain older, unmaintained games that rely on Intel-based
frameworks. Find out which macOS you’re using.
For optimal performance and future compatibility, you should update your
Intel-based apps, plug-ins, extensions, and other add-ons for Apple silicon.
"""
I do think to recall that the original plan was to discontinue Rosetta 2 with
the coming release (macOS 27 in 2026), but probably there were many complaints
by users and developers. A sentence like above "you should update your
Intel-based apps, plug-ins, extensions, and other add-ons for Apple silicon"
sounds rather non-constructive, with a considerable gap towards reality,
written by someone (or something) that is not involved in the truth behind
complex software systems.
Makarius
Email Gateway (Aug 30 2026 at 09:26):From: Mete Polat <mete@varto.ai>
From a PM with Makarius:
On 17/08/2026 22:46, Mete Polat wrote:
What’s the reason for z3 still requiring x86_64-darwin? Is it the only component left depending on Rosetta 2?
My understanding: SMT proof reconstruction depends on this particular old
version, and cannot easily be upgraded without redoing almost everything. The
plan is to do away with z3-smt proof reconstruction, and use veriT instead,
but that is not the whole story so far.Jasmin Blanchette and Martin Desharnais-Schäfer are the guys for that. It is
better to ask on the regular channels, to give them a chance to respond.
I finished creating a minimal port of the exact z3 revision for ARM, alongside the missing ARM versions of Nunchaku, SMBC, MiniSat, MiniSatProver, Lingeling and Plingeling, and CryptoMiniSat. I was able to build the AFP without Rosetta 2, so maybe we can completely finish the transition for Isabelle2026 to ARM MacOS?
I skipped porting CakeML which is required for two AFP theories. I think the port would take some time and it’s probably easier to just upgrade to the first version that also supports ARM builds. I assume the required changes to the two theories are reasonable.
What’s the preferred way to share the hermetic flox / nix environment that builds these components? Fine if I just append a zipped tar here? Or send a patch directly here?
Best,
Mete
On Aug 18, 2026, at 12:05 AM, Makarius <makarius@sketis.net> wrote:
On 17/08/2026 22:21, Makarius wrote:
Note that there have been significant changes for the desktop application launcher, both on macOS and Windows. Also note that macOS is now separate for Apple Silicon (ARM) versus Intel.
More notes concerning macOS ARM vs. Intel.Some months ago, I was under the impression that macOS 26 was the last version with Rosetta 2, for emulation of Intel on Apple Silicon (ARM) hardware, and that starting with "27" it will be discontinued --- meaning the macOS 27 release at the end of 2026.
Thus I made every effort to deliver a Isabelle2026 release that has arm64-darwin executables for everything, with the notable exclusion of z3 --- it needs further treatment in the near future.
I was wrong about the meaning of "27", because it will be macOS 28 in 2027, not macOS 27 in 2026. Apple grants one more release cycle for Intel-emulation: https://support.apple.com/en-us/102527
"""
Rosetta is currently available for any Mac with Apple silicon, and it will remain available through the forthcoming macOS 27 — the next major macOS release. Starting with computers using macOS 28, Rosetta functionality will be available only for certain older, unmaintained games that rely on Intel-based frameworks. Find out which macOS you’re using.For optimal performance and future compatibility, you should update your Intel-based apps, plug-ins, extensions, and other add-ons for Apple silicon.
"""I do think to recall that the original plan was to discontinue Rosetta 2 with the coming release (macOS 27 in 2026), but probably there were many complaints by users and developers. A sentence like above "you should update your Intel-based apps, plug-ins, extensions, and other add-ons for Apple silicon" sounds rather non-constructive, with a considerable gap towards reality, written by someone (or something) that is not involved in the truth behind complex software systems.
Makarius
Email Gateway (Aug 30 2026 at 11:46):From: Makarius <makarius@sketis.net>
On 30/08/2026 10:15, Mete Polat wrote:
I finished creating a minimal port of the exact z3 revision for ARM, alongside the missing ARM versions of Nunchaku, SMBC, MiniSat, MiniSatProver, Lingeling and Plingeling, and CryptoMiniSat.
Hi Mete,
we mainly need z3: Please send me any patches you have. It needs to be derived
from precisely the version that is specified in our README: Z3 4.4.0 unstable
(pre-release, revision 0482e7fe727c).
If you look at the Mercurial history of Isabelle/Admin/components/main, you
will see past attempts at arm64-linux that ultimately failed. Usually, all
arm64 platforms work the same.
Nunchaku and SMBC have no practical relevance. We have rather incomplete
platform coverage for this experiment anyway.
MiniSat already has a complete set of executables.
MiniSatProver, Lingeling and Plingeling, and CryptoMiniSat are not used by
Isabelle ---Where did you see them?
I was able to build the AFP without Rosetta 2
That helps to get an overview of the situation, but it is neither necessary
nor sufficient as a test.
AFP entries sometimes do odd things with the implicit assumption "running on
MY MACHINE with my tools installed".
I skipped porting CakeML which is required for two AFP theories.
The "cakeml-2.0" component is the tool context required to build cakeml
programs a long time ago. It looks like a private experiment by Lars Hupel:
https://github.com/isabelle-prover/cakeml-component --- with rather incomplete
platform coverage --- unmaintained.
What’s the preferred way to share the hermetic flox / nix environment that builds these components? Fine if I just append a zipped tar here? Or send a patch directly here?
I don't know anything about hermetic build environments.
Better see Isabelle/Admin/components/README.md --- there will be ultimately
some Isabelle/Scala tool like "isabelle component_XYZ".
All Isabelle tooling is done in Isabelle/Scala: that has already become a
tautology after so many years of Isabelle/Scala.
Makarius
Email Gateway (Aug 30 2026 at 15:51):From: Mete Polat <mete@varto.ai>
Hi Makarius,
I attached a patch with an Isabelle component. Thanks for the hint. Lmk if something is not working. It requires Python2, C and C++ compiler. I used Apple’s Xcode Command Line Tools for building.
Best,
Mete
isabelle-z3-arm64-darwin.patch
Email Gateway (Aug 30 2026 at 19:51):From: Lars Hupel <lars@hupel.info>
The "cakeml-2.0" component is the tool context required to build cakeml
programs a long time ago. It looks like a private experiment by Lars Hupel:
https://github.com/isabelle-prover/cakeml-component --- with rather
incomplete platform coverage --- unmaintained.
The platform coverage is restricted by what upstream offered at the
time: it contains a bootstrapped CakeML compiler as an assembly (.S)
file, which I downloaded and incorporated into the component.
It looks like upstream has an ARM version these days; however, porting
our Isabelle proofs to this new version is probably a Master's
thesis-level project.
(To add insult to injury, CakeML has discontinued the use of Lem, an
intermediate language to specify semantics, a long time ago. We relied
on that to obtain Isabelle definitions that are morally equivalent to
their HOL4 definitions.)
Email Gateway (Sep 28 2026 at 15:29):From: Makarius <makarius@sketis.net>
On 30/08/2026 17:14, Mete Polat wrote:
Hi Makarius,
I attached a patch with an Isabelle component. Thanks for the hint. Lmk if something is not working. It requires Python2, C and C++ compiler. I used Apple’s Xcode Command Line Tools for building.
Thank you for that: the key was to use clang (not gcc) and disable Intel sse
options on ARM. Trying further on arm64-linux, I've found trivial tweaks to
make it work, too.
The current result is Isabelle/10b1396ac4db and Isabelle/4b6b7a8f8858 ---
shortly after Isabelle2026-RC1. So we will test it on isabelle-dev, until the
next release candidate.
If that works out properly, we will have Isabelle2026 without any requirement
for Apple Intel emulation via Rosetta 2, and also have a complete arm64-linux
setup for the very first time.
Makarius
Email Gateway (Sep 28 2026 at 16:44):From: Mete Polat <mete@varto.ai>
On Sep 28, 2026, at 7:28 PM, Makarius <makarius@sketis.net> wrote:
On 30/08/2026 17:14, Mete Polat wrote:
Hi Makarius,
I attached a patch with an Isabelle component. Thanks for the hint. Lmk if something is not working. It requires Python2, C and C++ compiler. I used Apple’s Xcode Command Line Tools for building.
Thank you for that: the key was to use clang (not gcc) and disable Intel sse options on ARM. Trying further on arm64-linux, I've found trivial tweaks to make it work, too.The current result is Isabelle/10b1396ac4db and Isabelle/4b6b7a8f8858 --- shortly after Isabelle2026-RC1. So we will test it on isabelle-dev, until the next release candidate.
If that works out properly, we will have Isabelle2026 without any requirement for Apple Intel emulation via Rosetta 2, and also have a complete arm64-linux setup for the very first time.
Nice!
Makarius
Email Gateway (Sep 29 2026 at 09:49):From: Makarius <makarius@sketis.net>
On 29/09/2026 10:49, Mete Polat wrote:
If that works out properly, we will have Isabelle2026 without any
requirement for Apple Intel emulation via Rosetta 2, and also have a
complete arm64-linux setup for the very first time.
What’s missing for arm64-windows support?
Everything. We have nothing there, and it is a lot of work to keep an eye on
any platform.
I don't see arm64-windows becoming essential anytime soon: MS will have to do
the x86_64-windows emulation on there side, and I hope they will do it in the
long run, like they always did.
Note that for z3 there is even an ancient x86-windows executable, and it still
works. Apple has given up x86 very long ago.
Makarius
Email Gateway (Sep 29 2026 at 15:58):From: Mete Polat <mete@varto.ai>
On Sep 28, 2026, at 7:45 PM, Mete Polat <mete@varto.ai> wrote:
On Sep 28, 2026, at 7:28 PM, Makarius <makarius@sketis.net> wrote:
On 30/08/2026 17:14, Mete Polat wrote:
Hi Makarius,
I attached a patch with an Isabelle component. Thanks for the hint. Lmk if something is not working. It requires Python2, C and C++ compiler. I used Apple’s Xcode Command Line Tools for building.
Thank you for that: the key was to use clang (not gcc) and disable Intel sse options on ARM. Trying further on arm64-linux, I've found trivial tweaks to make it work, too.The current result is Isabelle/10b1396ac4db and Isabelle/4b6b7a8f8858 --- shortly after Isabelle2026-RC1. So we will test it on isabelle-dev, until the next release candidate.
If that works out properly, we will have Isabelle2026 without any requirement for Apple Intel emulation via Rosetta 2, and also have a complete arm64-linux setup for the very first time.
What’s missing for arm64-windows support?Nice!
Makarius
Email Gateway (Oct 03 2026 at 14:39):From: Makarius <makarius@sketis.net>
On 28/09/2026 17:28, Makarius wrote:
The current result is Isabelle/10b1396ac4db and Isabelle/4b6b7a8f8858 ---
shortly after Isabelle2026-RC1. So we will test it on isabelle-dev, until the
next release candidate.If that works out properly, we will have Isabelle2026 without any requirement
for Apple Intel emulation via Rosetta 2, and also have a complete arm64-linux
setup for the very first time.
After some days of testing and watching, I have now given up:
changeset: 85765:1594c52571e4
tag: tip
user: wenzelm
date: Sat Oct 03 16:25:35 2026 +0200
summary: revert most of 4b6b7a8f8858: arm64 binaries are unstable;
The situation is similar to what we have seen some years ago, when trying with
variations of arm64 builds, mostly on Linux.
Makarius
Email Gateway (Oct 03 2026 at 14:57):From: Makarius <makarius@sketis.net>
On 03/10/2026 16:39, Makarius wrote:
On 28/09/2026 17:28, Makarius wrote:
The current result is Isabelle/10b1396ac4db and Isabelle/4b6b7a8f8858 ---
shortly after Isabelle2026-RC1. So we will test it on isabelle-dev, until
the next release candidate.If that works out properly, we will have Isabelle2026 without any
requirement for Apple Intel emulation via Rosetta 2, and also have a
complete arm64-linux setup for the very first time.
After some days of testing and watching, I have now given up:changeset: 85765:1594c52571e4
tag: tip
user: wenzelm
date: Sat Oct 03 16:25:35 2026 +0200
summary: revert most of 4b6b7a8f8858: arm64 binaries are unstable;The situation is similar to what we have seen some years ago, when trying with
variations of arm64 builds, mostly on Linux.
More historical context:
changeset: 85725:4b6b7a8f8858
user: wenzelm
date: Mon Sep 28 15:56:27 2026 +0200
files: Admin/components/components.shasum Admin/components/main NEWS
src/Pure/ROOT.ML
description:
rebuild z3/0482e7fe727c for all platforms with current base-line OS versions,
including arm64-darwin and arm64-linux, but keep existing x86-windows binary;
enforce rebuild of Isabelle/ML;
Makarius
Last updated: Oct 08 2026 at 21:07 UTC