author | wenzelm |
Sat, 10 Dec 2016 15:45:16 +0100 | |
changeset 64544 | d23b7c9b9dd4 |
parent 61740 | d7e0315fe423 |
child 66691 | a8703e8ee1d3 |
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:
61136
diff
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:
61136
diff
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:
61136
diff
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:
61136
diff
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:
61136
diff
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:
61136
diff
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:
61136
diff
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:
61136
diff
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:
61136
diff
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:
61136
diff
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:
61136
diff
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:
61136
diff
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:
61136
diff
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:
61136
diff
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:
61136
diff
changeset
|
23 |
PLATFORMS="$ISABELLE_PLATFORM64 $ISABELLE_PLATFORM32" |
60983
ff4a67c65084
updated to polyml-5.5.3-20150820, with native x86-windows support;
wenzelm
parents:
56958
diff
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:
61136
diff
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:
61136
diff
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:
61136
diff
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:
61136
diff
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:
61136
diff
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:
61136
diff
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:
61136
diff
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:
61136
diff
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:
61136
diff
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:
61136
diff
changeset
|
38 |
then |
64544
d23b7c9b9dd4
updated Poly/ML repository test version (08-Dec-2016);
wenzelm
parents:
61740
diff
changeset
|
39 |
if "$POLYML_HOME/$PLATFORM/polyi" -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:
61136
diff
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:
61136
diff
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:
61136
diff
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:
61136
diff
changeset
|
43 |
|
64544
d23b7c9b9dd4
updated Poly/ML repository test version (08-Dec-2016);
wenzelm
parents:
61740
diff
changeset
|
44 |
ML_SYSTEM=polyml-5.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:
61136
diff
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:
61136
diff
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:
61136
diff
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:
61136
diff
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:
61136
diff
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:
61136
diff
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:
61136
diff
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:
61136
diff
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:
61136
diff
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:
61136
diff
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:
61136
diff
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:
61136
diff
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:
61136
diff
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:
61136
diff
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:
61136
diff
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:
61136
diff
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:
61136
diff
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:
61136
diff
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:
61136
diff
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:
61136
diff
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:
61136
diff
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:
61136
diff
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:
61136
diff
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:
61136
diff
changeset
|
69 |
unset PLATFORMS |