| author | wenzelm | 
| Thu, 14 Jul 2016 12:21:12 +0200 | |
| changeset 63491 | 58ccbc73a172 | 
| parent 61740 | d7e0315fe423 | 
| child 64544 | d23b7c9b9dd4 | 
| permissions | -rw-r--r-- | 
| 49000 | 1 | # -*- shell-script -*- :mode=shellscript: | 
| 2 | ||
| 53686 | 3 | POLYML_HOME="$COMPONENT" | 
| 4 | ||
| 5 | ||
| 61158 
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
 wenzelm parents: 
61136diff
changeset | 6 | # platform preference | 
| 49000 | 7 | |
| 61158 
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
 wenzelm parents: 
61136diff
changeset | 8 | if grep "ML_system_64.*=.*true" "$ISABELLE_HOME_USER/etc/preferences" >/dev/null 2>/dev/null | 
| 
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
 wenzelm parents: 
61136diff
changeset | 9 | then | 
| 
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
 wenzelm parents: 
61136diff
changeset | 10 | ML_SYSTEM_64="true" | 
| 
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
 wenzelm parents: 
61136diff
changeset | 11 | else | 
| 
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
 wenzelm parents: 
61136diff
changeset | 12 | ML_SYSTEM_64="false" | 
| 
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
 wenzelm parents: 
61136diff
changeset | 13 | fi | 
| 49000 | 14 | |
| 61158 
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
 wenzelm parents: 
61136diff
changeset | 15 | case "${ISABELLE_PLATFORM}:${ML_SYSTEM_64}" in
 | 
| 
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
 wenzelm parents: 
61136diff
changeset | 16 | x86-cygwin:true) | 
| 
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
 wenzelm parents: 
61136diff
changeset | 17 | PLATFORMS="x86_64-windows x86-windows" | 
| 49000 | 18 | ;; | 
| 61158 
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
 wenzelm parents: 
61136diff
changeset | 19 | x86-cygwin:*) | 
| 
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
 wenzelm parents: 
61136diff
changeset | 20 | PLATFORMS="x86-windows x86_64-windows" | 
| 
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
 wenzelm parents: 
61136diff
changeset | 21 | ;; | 
| 
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
 wenzelm parents: 
61136diff
changeset | 22 | *:true) | 
| 
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
 wenzelm parents: 
61136diff
changeset | 23 | PLATFORMS="$ISABELLE_PLATFORM64 $ISABELLE_PLATFORM32" | 
| 60983 
ff4a67c65084
updated to polyml-5.5.3-20150820, with native x86-windows support;
 wenzelm parents: 
56958diff
changeset | 24 | ;; | 
| 49000 | 25 | *) | 
| 61158 
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
 wenzelm parents: 
61136diff
changeset | 26 | PLATFORMS="$ISABELLE_PLATFORM32 $ISABELLE_PLATFORM64" | 
| 49000 | 27 | ;; | 
| 28 | esac | |
| 29 | ||
| 61158 
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
 wenzelm parents: 
61136diff
changeset | 30 | |
| 
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
 wenzelm parents: 
61136diff
changeset | 31 | # check executable | 
| 
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
 wenzelm parents: 
61136diff
changeset | 32 | |
| 
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
 wenzelm parents: 
61136diff
changeset | 33 | unset ML_HOME | 
| 
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
 wenzelm parents: 
61136diff
changeset | 34 | |
| 
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
 wenzelm parents: 
61136diff
changeset | 35 | for PLATFORM in $PLATFORMS | 
| 
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
 wenzelm parents: 
61136diff
changeset | 36 | do | 
| 
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
 wenzelm parents: 
61136diff
changeset | 37 | if [ -z "$ML_HOME" ] | 
| 
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
 wenzelm parents: 
61136diff
changeset | 38 | then | 
| 61161 
8fbab2f3433f
fully detached test run, to avoid flashing window on Windows with Cygwin-Terminal;
 wenzelm parents: 
61158diff
changeset | 39 | if "$POLYML_HOME/$PLATFORM/polyml" -v </dev/null >/dev/null 2>/dev/null | 
| 61158 
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
 wenzelm parents: 
61136diff
changeset | 40 | then | 
| 
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
 wenzelm parents: 
61136diff
changeset | 41 | |
| 
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
 wenzelm parents: 
61136diff
changeset | 42 | # ML settings | 
| 
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
 wenzelm parents: 
61136diff
changeset | 43 | |
| 61740 | 44 | ML_SYSTEM=polyml-5.6 | 
| 61158 
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
 wenzelm parents: 
61136diff
changeset | 45 | ML_PLATFORM="$PLATFORM" | 
| 
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
 wenzelm parents: 
61136diff
changeset | 46 | ML_HOME="$POLYML_HOME/$ML_PLATFORM" | 
| 
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
 wenzelm parents: 
61136diff
changeset | 47 | ML_SOURCES="$POLYML_HOME/src" | 
| 49000 | 48 | |
| 61158 
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
 wenzelm parents: 
61136diff
changeset | 49 | case "$ML_PLATFORM" in | 
| 
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
 wenzelm parents: 
61136diff
changeset | 50 | x86_64-windows) | 
| 
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
 wenzelm parents: 
61136diff
changeset | 51 | ML_OPTIONS="-H 1000 --codepage utf8" | 
| 
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
 wenzelm parents: 
61136diff
changeset | 52 | ;; | 
| 
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
 wenzelm parents: 
61136diff
changeset | 53 | x86-windows) | 
| 
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
 wenzelm parents: 
61136diff
changeset | 54 | ML_OPTIONS="-H 500 --codepage utf8" | 
| 
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
 wenzelm parents: 
61136diff
changeset | 55 | ;; | 
| 
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
 wenzelm parents: 
61136diff
changeset | 56 | x86_64-*) | 
| 
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
 wenzelm parents: 
61136diff
changeset | 57 | ML_OPTIONS="-H 1000" | 
| 
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
 wenzelm parents: 
61136diff
changeset | 58 | ;; | 
| 
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
 wenzelm parents: 
61136diff
changeset | 59 | *) | 
| 
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
 wenzelm parents: 
61136diff
changeset | 60 | ML_OPTIONS="-H 500" | 
| 
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
 wenzelm parents: 
61136diff
changeset | 61 | ;; | 
| 
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
 wenzelm parents: 
61136diff
changeset | 62 | esac | 
| 
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
 wenzelm parents: 
61136diff
changeset | 63 | |
| 
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
 wenzelm parents: 
61136diff
changeset | 64 | fi | 
| 
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
 wenzelm parents: 
61136diff
changeset | 65 | fi | 
| 
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
 wenzelm parents: 
61136diff
changeset | 66 | done | 
| 
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
 wenzelm parents: 
61136diff
changeset | 67 | |
| 
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
 wenzelm parents: 
61136diff
changeset | 68 | unset PLATFORM | 
| 
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
 wenzelm parents: 
61136diff
changeset | 69 | unset PLATFORMS |