Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
authorwenzelm
Fri, 11 Sep 2015 17:57:34 +0200
changeset 61158 ea6a4c8bc722
parent 61157 13f4056c42d7
child 61159 da900891ee06
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
Admin/components/components.sha1 file | annotate | diff | comparison | revisions
Admin/components/main file | annotate | diff | comparison | revisions
Admin/polyml/settings file | annotate | diff | comparison | revisions
NEWS file | annotate | diff | comparison | revisions
etc/options file | annotate | diff | comparison | revisions 
--- a/Admin/components/components.sha1	Fri Sep 11 17:48:49 2015 +0200
+++ b/Admin/components/components.sha1	Fri Sep 11 17:57:34 2015 +0200
@@ -94,6 +94,7 @@
 532f6e8814752aeb406c62fabcfd2cc05f8a7ca8  polyml-5.5.2.tar.gz
 1c53f699d35c0db6c7cf4ea51f2310adbd1d0dc5  polyml-5.5.3-20150820.tar.gz
 b4b624fb5f34d1dc814fb4fb469fafd7d7ea018a  polyml-5.5.3-20150908.tar.gz
+b668e1f43a41608a8eb365c5e19db6c54c72748a  polyml-5.5.3-20150911.tar.gz
 8ee375cfc38972f080dbc78f07b68dac03efe968  ProofGeneral-3.7.1.1.tar.gz
 847b52c0676b5eb0fbf0476f64fc08c2d72afd0c  ProofGeneral-4.1.tar.gz
 8e0b2b432755ef11d964e20637d1bc567d1c0477  ProofGeneral-4.2-1.tar.gz
--- a/Admin/components/main	Fri Sep 11 17:48:49 2015 +0200
+++ b/Admin/components/main	Fri Sep 11 17:57:34 2015 +0200
@@ -9,7 +9,7 @@
 jfreechart-1.0.14-1
 jortho-1.0-2
 kodkodi-1.5.2
-polyml-5.5.3-20150908
+polyml-5.5.3-20150911
 scala-2.11.7
 spass-3.8ds
 xz-java-1.2-1
--- a/Admin/polyml/settings	Fri Sep 11 17:48:49 2015 +0200
+++ b/Admin/polyml/settings	Fri Sep 11 17:57:34 2015 +0200
@@ -3,56 +3,67 @@
 POLYML_HOME="$COMPONENT"
 
 
-# simple settings (example)
+# platform preference
 
-#ML_SYSTEM=polyml-5.5.3
-#ML_PLATFORM="$ISABELLE_PLATFORM32"
-#ML_HOME="$POLYML_HOME/$ML_PLATFORM"
-#ML_OPTIONS="-H 500"
-#ML_SOURCES="$POLYML_HOME/src"
-
-
-# smart settings
-
-ML_SYSTEM=polyml-5.5.3
+if grep "ML_system_64.*=.*true" "$ISABELLE_HOME_USER/etc/preferences" >/dev/null 2>/dev/null
+then
+  ML_SYSTEM_64="true"
+else
+  ML_SYSTEM_64="false"
+fi
 
-case "$ISABELLE_PLATFORM" in
-  *-linux)
-    if env LD_LIBRARY_PATH="$POLYML_HOME/$ISABELLE_PLATFORM32:$LD_LIBRARY_PATH" \
-      "$POLYML_HOME/$ISABELLE_PLATFORM32/poly" -v >/dev/null 2>/dev/null
-    then
-      ML_PLATFORM="$ISABELLE_PLATFORM32"
-    else
-      ML_PLATFORM="$ISABELLE_PLATFORM64"
-      if [ -z "$ML_PLATFORM_FALLBACK" ]; then
-        echo >&2 "### Cannot execute Poly/ML in 32bit mode (missing shared libraries for C/C++)"
-        echo >&2 "### Using bulky 64bit version of Poly/ML instead"
-        ML_PLATFORM_FALLBACK="true"
-      fi
-    fi
+case "${ISABELLE_PLATFORM}:${ML_SYSTEM_64}" in
+  x86-cygwin:true)
+    PLATFORMS="x86_64-windows x86-windows"
     ;;
-  x86-cygwin)
-    ML_PLATFORM="x86-windows"
+  x86-cygwin:*)
+    PLATFORMS="x86-windows x86_64-windows"
+    ;;
+  *:true)
+    PLATFORMS="$ISABELLE_PLATFORM64 $ISABELLE_PLATFORM32"
     ;;
   *)
-    ML_PLATFORM="$ISABELLE_PLATFORM32"
+    PLATFORMS="$ISABELLE_PLATFORM32 $ISABELLE_PLATFORM64"
     ;;
 esac
 
-case "$ML_PLATFORM" in
-  x86_64-windows)
-    ML_OPTIONS="-H 1000 --codepage utf8"
-    ;;
-  x86-windows)
-    ML_OPTIONS="-H 500 --codepage utf8"
-    ;;
-  x86_64-*)
-    ML_OPTIONS="-H 1000"
-    ;;
-  *)
-    ML_OPTIONS="-H 500"
-    ;;
-esac
+
+# check executable
+
+unset ML_HOME
+
+for PLATFORM in $PLATFORMS
+do
+  if [ -z "$ML_HOME" ]
+  then
+    if "$POLYML_HOME/$PLATFORM/polyml" -v >/dev/null 2>/dev/null
+    then
+
+      # ML settings
+
+      ML_SYSTEM=polyml-5.5.3
+      ML_PLATFORM="$PLATFORM"
+      ML_HOME="$POLYML_HOME/$ML_PLATFORM"
+      ML_SOURCES="$POLYML_HOME/src"
 
-ML_HOME="$POLYML_HOME/$ML_PLATFORM"
-ML_SOURCES="$POLYML_HOME/src"
+      case "$ML_PLATFORM" in
+        x86_64-windows)
+          ML_OPTIONS="-H 1000 --codepage utf8"
+          ;;
+        x86-windows)
+          ML_OPTIONS="-H 500 --codepage utf8"
+          ;;
+        x86_64-*)
+          ML_OPTIONS="-H 1000"
+          ;;
+        *)
+          ML_OPTIONS="-H 500"
+          ;;
+      esac
+
+    fi
+  fi
+done
+
+unset PLATFORM
+unset PLATFORMS
--- a/NEWS	Fri Sep 11 17:48:49 2015 +0200
+++ b/NEWS	Fri Sep 11 17:57:34 2015 +0200
@@ -344,6 +344,10 @@
 
 *** System ***
 
+* Poly/ML default platform architecture may be changed from 32bit to
+64bit via system option ML_system_64. A system restart (and rebuild)
+is required after change.
+
 * Poly/ML 5.5.3 runs natively on x86-windows and x86_64-windows,
 which both allow larger heap space than former x86-cygwin.
 
--- a/etc/options	Fri Sep 11 17:48:49 2015 +0200
+++ b/etc/options	Fri Sep 11 17:57:34 2015 +0200
@@ -107,6 +107,9 @@
 public option ML_statistics : bool = true
   -- "ML run-time system statistics"
 
+public option ML_system_64 : bool = false
+  -- "ML system for 64bit platform is used if possible (change requires restart)"
+
 
 section "Editor Reactivity"
isabelle