| author | paulson <lp15@cam.ac.uk> | 
| Sun, 06 May 2018 23:59:01 +0100 | |
| changeset 68096 | e58c9ac761cb | 
| parent 67581 | 30f412d1d7c3 | 
| child 69704 | 3fb94d9b87b0 | 
| 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  | 
|
| 66761 | 15  | 
case "${ISABELLE_PLATFORM_FAMILY}:${ML_SYSTEM_64}" in
 | 
16  | 
windows:true)  | 
|
| 
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
 | 
17  | 
PLATFORMS="x86_64-windows x86-windows"  | 
| 49000 | 18  | 
;;  | 
| 66761 | 19  | 
windows:*)  | 
| 
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
 | 
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  | 
| 
67581
 
30f412d1d7c3
removed obsolete polyi executable: change of DYLD_LIBRARY_PATH is not required;
 
wenzelm 
parents: 
67099 
diff
changeset
 | 
39  | 
if "$POLYML_HOME/$PLATFORM/poly" -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  | 
|
| 66761 | 44  | 
ML_SYSTEM=polyml-5.7.1  | 
| 
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)  | 
| 67017 | 51  | 
ML_OPTIONS="--minheap 1000 --codepage utf8"  | 
| 
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
 | 
52  | 
;;  | 
| 67099 | 53  | 
x86-windows)  | 
54  | 
ML_OPTIONS="--minheap 500 --codepage utf8"  | 
|
55  | 
;;  | 
|
| 
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
 | 
56  | 
x86_64-*)  | 
| 67099 | 57  | 
ML_OPTIONS="--minheap 1000"  | 
| 
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
 | 
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  | 
*)  | 
| 67099 | 60  | 
ML_OPTIONS="--minheap 500"  | 
| 
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
 | 
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  |