Stream: Mirror: Isabelle Development Mailing List

Topic: NEWS: update to mlton-20241230-2

Email Gateway (Oct 02 2026 at 21:51):

From: Makarius <makarius@sketis.net>

* System *

• The Isabelle component for the MLton compiler now covers all platform
  variants for Linux and macOS (x86_64 and arm64), but still not Windows.
  ISABELLE_MLTON_OPTIONS are empty by default, but may be overridden in
  $ISABELLE_HOME_USER/etc/settings; new ISABELLE_MLTON_NATIVE_OPTIONS
  enable "-codegen native" on x86_64, but not on arm64. Mlton requires a C
  compiler with libgmp, as before.

This refers to Isabelle/4370df23614d. It is still the old mlton-20241230-1,
but with slightly different binaries from the new Github home of the project.
I have tested the Mlton applications in AFP/b9b19405ddc3 on x64_64-linux and
arm64-darwin like this:

isabelle build -A: PAC_Checker Munta_Model_Checker
Munta_Certificate_Checker Native_Word Buchi_Complementation

For arm64-linux it should work in principle, but I need a better test machine:
probably Docker on Apple hardware, which I did not try yet.

For x86_64-windows, I did not do anything. There are now binaries for various
C compilers, including Msys2 / UCRT64. It should eventually work, but there is
no time now.

Makarius

Email Gateway (Oct 03 2026 at 14:44):

From: Makarius <makarius@sketis.net>

On 02/10/2026 23:50, Makarius wrote:

isabelle build -A: PAC_Checker Munta_Model_Checker
Munta_Certificate_Checker Native_Word Buchi_Complementation

For arm64-linux it should work in principle, but I need a better test machine:
probably Docker on Apple hardware, which I did not try yet.

After some experimentation, it did work quite well with Podman
https://podman.io instead of Docker. So Mlton looks fine on arm64-linux now,
but z3 doesn't. Most of the above applications required (smt (z3)), but that
is too unstable on arm64-linux (see Isabelle/65f981cf4474).

Makarius

Last updated: Oct 05 2026 at 16:54 UTC