Stream: Mirror: Isabelle Development Mailing List

Topic: NEWS: Separate application bundles for "macos" (Intel) vs...

Email Gateway (Jul 14 2026 at 22:08):

From: Makarius <makarius@sketis.net>
Subject: NEWS: Separate application bundles for "macos" (Intel) vs. "macos_arm" (Apple Silicon)

* General *

• The Isabelle application bundle has been split into "macos"
  (x86_64-darwin, Intel) and "macos_arm (arm64-darwin, Apple Silicon). The
  correct version needs to be used for the actual system platform:
  emulated Java via Rosetta 2 is explicitly excluded. Isabelle add-on
  tools usually work on arm64-darwin, with the notable exception of the z3
  prover --- z3 uses x86_64-darwin and thus requires Rosetta 2, as long as
  that is still provided by Apple.

This refers to Isabelle/ca65aeef65f0.

Here is the complete list of remaining x86_64 tools:

- z3 (stuck with a very old side-branch of the sources)
- nunchaku + smbc (considered "experimental", not used in applications)

The list used to have further entries, but they are now native on arm64:

- spass-3.8ds: after closer inspection, I managed to re-build it on all
current platforms (see also "isabelle component_spass" in
Isabelle/272abac962eb and preceeding changes).

- vampire-4.8: that is a dead side-branch before current vampire-5,
specifically for Isabelle ("HO" + "sledgehammer"). I was rather lucky to
rebuild it for arm64-darwin on one of my old macOS installations: actually a
cross-compile from Intel, which explains minor misunderstandings in the
changelog of Isabelle/8eee497c7252).

That's finally it for the coming Isabelle release. Note that next year's macOS
release will no longer support arm64 + x86_64 side-by-side. (The "27" release
of 2026 still does, despite the confusion of numbers.)

Makarius

Email Gateway (Jul 14 2026 at 22:31):

From: Makarius <makarius@sketis.net>
Subject: NEWS: Separate application bundles for "macos" (Intel) vs. "macos_arm" (Apple Silicon)

On 15/07/2026 00:07, Makarius wrote:

The list used to have further entries, but they are now native on arm64:

- spass-3.8ds: after closer inspection, I managed to re-build it on all
current platforms (see also "isabelle component_spass" in
Isabelle/272abac962eb and preceeding changes).

- vampire-4.8: that is a dead side-branch before current vampire-5,
specifically for Isabelle ("HO" + "sledgehammer"). I was rather lucky to
rebuild it for arm64-darwin on one of my old macOS installations: actually a
cross-compile from Intel, which explains minor misunderstandings in the
changelog of Isabelle/8eee497c7252).

One more entry:

- zipperposition-2.1: I managed to tinker with opam-2.2.1 instead of our
usual opam-2.0.7, see also Isabelle/85ee34305702.

We are stuck with opam-2.0.7, the last version that was available for Cygwin.
Later opam-2.2.1 theoretically supports Windows better, via Msys2 instead of
Cygwin, but I did not quite manage to make it work for us. The OCaml ecosystem
is generally a bit fragile an not quite portable.

Makarius

Last updated: Aug 05 2026 at 21:11 UTC