suppress arm64-darwin, which does not support "-codegen native" (required for AFP/PAC_Checker);
clarified NEWS;
--- a/Admin/components/components.sha1 Thu Mar 21 16:54:53 2024 +0100
+++ b/Admin/components/components.sha1 Thu Mar 21 21:03:06 2024 +0100
@@ -316,6 +316,7 @@
ae76bfaade3bf72ff6b2d3aafcd52fa45609fcd1 minisat-2.2.1.tar.gz
59aa13f48685326995714cc6028aebb789e445e3 mlton-20210117-1.tar.gz
7624509ba58b9b8231626a66eda571fba69f7cd3 mlton-20210117-2.tar.gz
+2d8c08fc623e7643a10ee031c7e9e7cb7c01d53a mlton-20210117-3.tar.gz
5d48b7163a68c18b691bedc1511364b0b103baeb mlton-20210117.tar.gz
eda10c62da927a842c0a8881f726eac85e1cb4f7 naproche-20210122.tar.gz
edcb517b7578db4eec1b6573b624f291776e11f6 naproche-20210124.tar.gz
--- a/Admin/components/main Thu Mar 21 16:54:53 2024 +0100
+++ b/Admin/components/main Thu Mar 21 21:03:06 2024 +0100
@@ -22,7 +22,7 @@
lipics-3.1.3
llncs-2.23
minisat-2.2.1-1
-mlton-20210117-2
+mlton-20210117-3
nunchaku-0.5
opam-2.0.7
pdfjs-2.14.305
--- a/NEWS Thu Mar 21 16:54:53 2024 +0100
+++ b/NEWS Thu Mar 21 21:03:06 2024 +0100
@@ -238,10 +238,10 @@
component javamail (previously javax.mail) from jakarta 2.1.2
using eclipse angus 2.0.2/2.0.1.
-* The MLton compiler has been bundled as Isabelle component, for
-x86_64-linux, x86_64-darwin, arm64-darwin. ISABELLE_MLTON_OPTIONS that
-work most of the time are provided by default, but this may have to be
-overridden (e.g. in $ISABELLE_HOME_USER/etc/settings).
+* The Isabelle component for the MLton compiler now covers macOS and
+Linux (Intel), while Windows and Linux (ARM) are unsupported. The
+default for ISABELLE_MLTON_OPTIONS should work most of the time, but may
+have to be overridden (e.g. in $ISABELLE_HOME_USER/etc/settings).
* Update to GHC stack 2.15.1 with support for all platforms, including
ARM Linux and Apple Silicon.
--- a/src/Pure/Admin/component_mlton.scala Thu Mar 21 16:54:53 2024 +0100
+++ b/src/Pure/Admin/component_mlton.scala Thu Mar 21 21:03:06 2024 +0100
@@ -20,7 +20,6 @@
val platforms: List[Download_Platform] =
List(
- Download_Platform("arm64-darwin", "arm64-darwin-21.6-gmp-static.tgz"),
Download_Platform("x86_64-darwin", "amd64-darwin-16.7-gmp-static.tgz"),
Download_Platform("x86_64-linux", "amd64-linux-glibc2.19-gmp-static.tgz"))
@@ -64,8 +63,8 @@
/* settings */
component_dir.write_settings("""
-if [ -d "$COMPONENT/${ISABELLE_APPLE_PLATFORM64:-$ISABELLE_PLATFORM64}" ]; then
- ISABELLE_MLTON="$COMPONENT/${ISABELLE_APPLE_PLATFORM64:-$ISABELLE_PLATFORM64}/bin/mlton"
+if [ -d "$COMPONENT/$ISABELLE_PLATFORM64" ]; then
+ ISABELLE_MLTON="$COMPONENT/$ISABELLE_PLATFORM64/bin/mlton"
case "$ISABELLE_PLATFORM_FAMILY" in
linux*)
ISABELLE_MLTON_OPTIONS="-pi-style npi"
@@ -84,7 +83,7 @@
"""This distribution of MLton has been taken from the TINA project
https://projects.laas.fr/tina/software.php using following downloads:""" +
platforms.map(_.download(base_url, version)).mkString("\n\n ", "\n ", "\n\n") +
-"""Some Isabelle platforms are unsupported, notably Windows and Linux ARM.
+"""Windows and Linux ARM are unsupported.
Makarius