# HG changeset patch # User wenzelm # Date 1441987054 -7200 # Node ID ea6a4c8bc722906693357292a2d3b0b293a155f4 # Parent 13f4056c42d7e3db79247746e1cc31d74715efad convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap; diff -r 13f4056c42d7 -r ea6a4c8bc722 Admin/components/components.sha1 --- 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 diff -r 13f4056c42d7 -r ea6a4c8bc722 Admin/components/main --- 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 diff -r 13f4056c42d7 -r ea6a4c8bc722 Admin/polyml/settings --- 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 diff -r 13f4056c42d7 -r ea6a4c8bc722 NEWS --- 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. diff -r 13f4056c42d7 -r ea6a4c8bc722 etc/options --- 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"