Stream: Mirror: Isabelle Development Mailing List

Topic: NEWS: update to MLton 20241230

Email Gateway (Feb 03 2025 at 20:10):

From: Makarius <makarius@sketis.net>
* System *

• Update of the MLton SML compiler to work better with current macOS
  versions (including ARM): this requires a C compiler and libgmp. Windows
  and Linux ARM remain unsupported, as before.

This refers to Isabelle/f178475f274d.

MLton is important for code generation from HOL to Standard ML. In the past
2-3 years, the release situation did not look good, but just a few weeks ago,
someone has published up-to-date builds for recent OS / HW. See also
https://sourceforge.net/projects/mlton/files/mlton/20241230

Thus we are lucky, and don't have to produce our own Isabelle build tools for
MLton.

Makarius

Last updated: Apr 18 2025 at 20:21 UTC