NEWS: update to MLton 20241230
Makarius
makarius at sketis.net
Mon Feb 3 21:09:31 CET 2025
*** 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
More information about the isabelle-dev
mailing list