suppress arm64-darwin, which does not support "-codegen native" (required for AFP/PAC_Checker);
authorwenzelm
Thu, 21 Mar 2024 21:03:06 +0100
changeset 79961 2b9205301ff5
parent 79960 7747a8efcad0
child 79962 26592fe88250
suppress arm64-darwin, which does not support "-codegen native" (required for AFP/PAC_Checker); clarified NEWS;
Admin/components/components.sha1
Admin/components/main
NEWS
src/Pure/Admin/component_mlton.scala
--- 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