Email Gateway (Sep 20 2026 at 13:09): Email Gateway (Sep 20 2026 at 13:09):From: "Thiemann, René" <cl-isabelle-users@lists.cam.ac.uk>
Subject: [isabelle] Isabelle2026-RC1 available for testing: z3 problems with MacOS 27
Dear Makarius, dear all,
thank you for putting together Isabelle 2026 RC1.
After trying a fresh install of Isabelle 2026-RC1 on a fresh MacOS Golden Gate 27.0,
there is the problem that z3 is not working out of the box.
This problem already appears when trying to build AFP entries, e.g.
*** Solver z3: Solver terminated abnormally with error code 126
*** At command "by" (line 52 of "$AFP/First_Order_Terms/Unification_More.thy")
*** Solver z3: Solver terminated abnormally with error code 126
*** At command "by" (line 178 of "$AFP/First_Order_Terms/Term_Impl.thy")
On a prompt, I receive:
$ /Applications/Isabelle2026-RC1.app/contrib/z3-4.4.0pre-6/x86_64-darwin/z3
-bash: /Applications/Isabelle2026-RC1.app/contrib/z3-4.4.0pre-6/x86_64-darwin/z3: Bad CPU type in executable
When installing Rosetta manually, then everything works fine again, but the fact that Rosetta needs to be
installed is not listed on the installation instructions.
https://isabelle.in.tum.de/website-Isabelle2026-RC1/installation.html
In my view, this situation should be improved by either stating this requirement more prominently
on the installation website, or by somehow configuring the Isabelle.app in a way that
on startup it checks whether Rosetta is installed, and otherwise complains immediately.
Best,
René
Am 19.09.2026 um 23:56 schrieb Makarius <makarius@sketis.net>:
Dear Isabelle users,
according to the plan https://sketis.net/2025/plan-for-isabelle2026-october-2026 we are now ready to start the release process for Isabelle2026 (October 2026). See also the continuously updated blog post https://sketis.net/2026/release-candidates-for-isabelle2026
The current release candidate is available from https://isabelle.in.tum.de/website-Isabelle2026-RC1
A corresponding version of the Archive of Formal Proofs is https://foss.heptapod.net/isa-afp/afp-devel/-/commit/9899990d74b6
Almost everything is ready for testing. See the NEWS and ANNOUNCE files as usual.
We now have approx. 4-5 weeks of thorough testing of release candidates, until a final and unchangeable release will emerge.
Any feedback about Isabelle release candidates should be posted with a meaningful Mail subject, not just a clone of this announcement.
Makarius
Email Gateway (Sep 27 2026 at 20:14):From: Makarius <makarius@sketis.net>
Subject: [isabelle] Isabelle2026-RC1 available for testing: z3 problems with MacOS 27
On 20/09/2026 15:09, Thiemann, René (via cl-isabelle-users Mailing List) wrote:
On a prompt, I receive:
$ /Applications/Isabelle2026-RC1.app/contrib/z3-4.4.0pre-6/x86_64-darwin/z3
-bash: /Applications/Isabelle2026-RC1.app/contrib/z3-4.4.0pre-6/x86_64-darwin/z3: Bad CPU type in executableWhen installing Rosetta manually, then everything works fine again, but the fact that Rosetta needs to be
installed is not listed on the installation instructions.https://isabelle.in.tum.de/website-Isabelle2026-RC1/installation.html
In my view, this situation should be improved by either stating this requirement more prominently
on the installation website, or by somehow configuring the Isabelle.app in a way that
on startup it checks whether Rosetta is installed, and otherwise complains immediately.
For now, I have merely updated installation.html, but probably nobody will
look there.
We used to have an explicit request for Rosetta on the desktop app, but I
removed that, to make it work without Intel emulation from the start. (Apple
intends to discontinue for macOS 28.)
There could be other feedback on startup, but before doing anything, I will
give one last try on z3, based on the proposal by Mete Polat from 30-Aug-2026.
(I've now spent 5min to look at it for the very first time.)
Makarius
Last updated: Oct 08 2026 at 21:07 UTC