1 # -*- shell-script -*- :mode=shellscript: |
1 # -*- shell-script -*- :mode=shellscript: |
2 |
2 |
3 POLYML_HOME="$COMPONENT" |
3 POLYML_HOME="$COMPONENT" |
4 |
4 |
5 |
5 |
6 # simple settings (example) |
6 # platform preference |
7 |
7 |
8 #ML_SYSTEM=polyml-5.5.3 |
8 if grep "ML_system_64.*=.*true" "$ISABELLE_HOME_USER/etc/preferences" >/dev/null 2>/dev/null |
9 #ML_PLATFORM="$ISABELLE_PLATFORM32" |
9 then |
10 #ML_HOME="$POLYML_HOME/$ML_PLATFORM" |
10 ML_SYSTEM_64="true" |
11 #ML_OPTIONS="-H 500" |
11 else |
12 #ML_SOURCES="$POLYML_HOME/src" |
12 ML_SYSTEM_64="false" |
|
13 fi |
13 |
14 |
14 |
15 case "${ISABELLE_PLATFORM}:${ML_SYSTEM_64}" in |
15 # smart settings |
16 x86-cygwin:true) |
16 |
17 PLATFORMS="x86_64-windows x86-windows" |
17 ML_SYSTEM=polyml-5.5.3 |
|
18 |
|
19 case "$ISABELLE_PLATFORM" in |
|
20 *-linux) |
|
21 if env LD_LIBRARY_PATH="$POLYML_HOME/$ISABELLE_PLATFORM32:$LD_LIBRARY_PATH" \ |
|
22 "$POLYML_HOME/$ISABELLE_PLATFORM32/poly" -v >/dev/null 2>/dev/null |
|
23 then |
|
24 ML_PLATFORM="$ISABELLE_PLATFORM32" |
|
25 else |
|
26 ML_PLATFORM="$ISABELLE_PLATFORM64" |
|
27 if [ -z "$ML_PLATFORM_FALLBACK" ]; then |
|
28 echo >&2 "### Cannot execute Poly/ML in 32bit mode (missing shared libraries for C/C++)" |
|
29 echo >&2 "### Using bulky 64bit version of Poly/ML instead" |
|
30 ML_PLATFORM_FALLBACK="true" |
|
31 fi |
|
32 fi |
|
33 ;; |
18 ;; |
34 x86-cygwin) |
19 x86-cygwin:*) |
35 ML_PLATFORM="x86-windows" |
20 PLATFORMS="x86-windows x86_64-windows" |
|
21 ;; |
|
22 *:true) |
|
23 PLATFORMS="$ISABELLE_PLATFORM64 $ISABELLE_PLATFORM32" |
36 ;; |
24 ;; |
37 *) |
25 *) |
38 ML_PLATFORM="$ISABELLE_PLATFORM32" |
26 PLATFORMS="$ISABELLE_PLATFORM32 $ISABELLE_PLATFORM64" |
39 ;; |
27 ;; |
40 esac |
28 esac |
41 |
29 |
42 case "$ML_PLATFORM" in |
|
43 x86_64-windows) |
|
44 ML_OPTIONS="-H 1000 --codepage utf8" |
|
45 ;; |
|
46 x86-windows) |
|
47 ML_OPTIONS="-H 500 --codepage utf8" |
|
48 ;; |
|
49 x86_64-*) |
|
50 ML_OPTIONS="-H 1000" |
|
51 ;; |
|
52 *) |
|
53 ML_OPTIONS="-H 500" |
|
54 ;; |
|
55 esac |
|
56 |
30 |
57 ML_HOME="$POLYML_HOME/$ML_PLATFORM" |
31 # check executable |
58 ML_SOURCES="$POLYML_HOME/src" |
32 |
|
33 unset ML_HOME |
|
34 |
|
35 for PLATFORM in $PLATFORMS |
|
36 do |
|
37 if [ -z "$ML_HOME" ] |
|
38 then |
|
39 if "$POLYML_HOME/$PLATFORM/polyml" -v >/dev/null 2>/dev/null |
|
40 then |
|
41 |
|
42 # ML settings |
|
43 |
|
44 ML_SYSTEM=polyml-5.5.3 |
|
45 ML_PLATFORM="$PLATFORM" |
|
46 ML_HOME="$POLYML_HOME/$ML_PLATFORM" |
|
47 ML_SOURCES="$POLYML_HOME/src" |
|
48 |
|
49 case "$ML_PLATFORM" in |
|
50 x86_64-windows) |
|
51 ML_OPTIONS="-H 1000 --codepage utf8" |
|
52 ;; |
|
53 x86-windows) |
|
54 ML_OPTIONS="-H 500 --codepage utf8" |
|
55 ;; |
|
56 x86_64-*) |
|
57 ML_OPTIONS="-H 1000" |
|
58 ;; |
|
59 *) |
|
60 ML_OPTIONS="-H 500" |
|
61 ;; |
|
62 esac |
|
63 |
|
64 fi |
|
65 fi |
|
66 done |
|
67 |
|
68 unset PLATFORM |
|
69 unset PLATFORMS |