author | wenzelm |
Wed, 09 May 2018 22:03:02 +0200 | |
changeset 68131 | 62a3294edda3 |
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 |