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