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.)
Last updated: Sep 02 2026 at 16:10 UTC