support for system option ML_system_apple: emulated x86_64 Poly/ML is sometimes more stable than native ARM64;
authorwenzelm
Wed, 12 Oct 2022 11:15:36 +0200
changeset 76275 b446004b2464
parent 76274 793171d7800b
child 76276 13b733e78c26
support for system option ML_system_apple: emulated x86_64 Poly/ML is sometimes more stable than native ARM64;
Admin/components/main
Admin/polyml/settings
NEWS
etc/options
src/Pure/Admin/build_release.scala
--- a/Admin/components/main	Sun Oct 09 16:28:28 2022 +0200
+++ b/Admin/components/main	Wed Oct 12 11:15:36 2022 +0200
@@ -20,7 +20,7 @@
 nunchaku-0.5
 opam-2.0.7
 pdfjs-2.14.305
-polyml-test-bafe319bc3a6
+polyml-test-bafe319bc3a6-1
 postgresql-42.5.0
 scala-3.2.0
 smbc-0.4.1
--- a/Admin/polyml/settings	Sun Oct 09 16:28:28 2022 +0200
+++ b/Admin/polyml/settings	Wed Oct 12 11:15:36 2022 +0200
@@ -2,7 +2,17 @@
 
 POLYML_HOME="$COMPONENT"
 
-ML_PLATFORM="${ISABELLE_APPLE_PLATFORM64:-${ISABELLE_WINDOWS_PLATFORM64:-${ISABELLE_PLATFORM64}}}"
+if [ -n "$ISABELLE_APPLE_PLATFORM64" ]
+then
+  if grep "ML_system_apple.*=.*false" "$ISABELLE_HOME_USER/etc/preferences" >/dev/null 2>/dev/null
+  then
+    ML_PLATFORM="$ISABELLE_PLATFORM64"
+  else
+    ML_PLATFORM="$ISABELLE_APPLE_PLATFORM64"
+  fi
+else
+  ML_PLATFORM="${ISABELLE_WINDOWS_PLATFORM64:-$ISABELLE_PLATFORM64}"
+fi
 
 if grep "ML_system_64.*=.*true" "$ISABELLE_HOME_USER/etc/preferences" >/dev/null 2>/dev/null
 then
--- a/NEWS	Sun Oct 09 16:28:28 2022 +0200
+++ b/NEWS	Wed Oct 12 11:15:36 2022 +0200
@@ -416,6 +416,11 @@
 together. Potential INCOMPATIBILITY for existing
 $ISABELLE_HOME_USER/etc/settings.
 
+* The system option "ML_system_apple" controls the use of native
+Apple/ARM64 for Poly/ML: default "true". Like "ML_system_64" this only
+works when saved in "$ISABELLE_HOME_USER/etc/preferences" (e.g. after
+shutdown of Isabelle/jEdit).
+
 
 
 New in Isabelle2021-1 (December 2021)
--- a/etc/options	Sun Oct 09 16:28:28 2022 +0200
+++ b/etc/options	Wed Oct 12 11:15:36 2022 +0200
@@ -163,6 +163,9 @@
 public option ML_system_64 : bool = false
   -- "ML system for 64bit platform is used if possible (change requires restart)"
 
+public option ML_system_apple : bool = true
+  -- "prefer native Apple/ARM64 platform (change requires restart)"
+
 public option ML_process_policy : string = ""
   -- "ML process command prefix (process policy)"
 
--- a/src/Pure/Admin/build_release.scala	Sun Oct 09 16:28:28 2022 +0200
+++ b/src/Pure/Admin/build_release.scala	Wed Oct 12 11:15:36 2022 +0200
@@ -249,7 +249,8 @@
               "cd " + File.bash_path(remote_dir),
               "tar -xf tmp.tar",
               build_command,
-              """perl -pi -e "s/ISABELLE_APPLE_PLATFORM64/ISABELLE_WINDOWS_PLATFORM64/g;" "$(bin/isabelle getenv -b POLYML_HOME)/etc/settings" """,
+              """mkdir -p "$(bin/isabelle getenv -b ISABELLE_HOME_USER)/etc" """,
+              """{ echo "ML_system_apple = false" > "$(bin/isabelle getenv -b ISABELLE_HOME_USER)/etc/preferences"; }""",
               build_command,
               "tar -cf tmp.tar heaps")
           ssh.execute(build_script.mkString(" && "), settings = false).check