14 # ML_HOME specifies the location of the actual compiler binaries. Do |
14 # ML_HOME specifies the location of the actual compiler binaries. Do |
15 # not invent new ML system names unless you know what you are doing. |
15 # not invent new ML system names unless you know what you are doing. |
16 # Only one of the sections below should be activated. |
16 # Only one of the sections below should be activated. |
17 |
17 |
18 # Poly/ML 5.x (automated settings) |
18 # Poly/ML 5.x (automated settings) |
19 POLY_HOME="$(type -p poly)"; [ -n "$POLY_HOME" ] && POLY_HOME="$(dirname "$POLY_HOME")" |
|
20 ML_PLATFORM="$ISABELLE_PLATFORM" |
19 ML_PLATFORM="$ISABELLE_PLATFORM" |
21 ML_HOME="$(choosefrom \ |
20 ML_HOME="$(choosefrom \ |
22 "$ISABELLE_HOME/contrib/polyml/$ML_PLATFORM" \ |
21 "$ISABELLE_HOME/contrib/polyml/$ML_PLATFORM" \ |
23 "$ISABELLE_HOME/../polyml/$ML_PLATFORM" \ |
22 "$ISABELLE_HOME/../polyml/$ML_PLATFORM" \ |
24 "/usr/local/polyml/$ML_PLATFORM" \ |
23 "/usr/local/polyml/$ML_PLATFORM" \ |
25 "/usr/share/polyml/$ML_PLATFORM" \ |
24 "/usr/share/polyml/$ML_PLATFORM" \ |
26 "/opt/polyml/$ML_PLATFORM" \ |
25 "/opt/polyml/$ML_PLATFORM" \ |
27 "$POLY_HOME")" |
26 "")" |
28 ML_SYSTEM=$("$ISABELLE_HOME/lib/scripts/polyml-version") |
27 ML_SYSTEM=$("$ISABELLE_HOME/lib/scripts/polyml-version") |
29 ML_OPTIONS="-H 200" |
28 ML_OPTIONS="-H 200" |
30 ML_SOURCES="$ML_HOME/../src" |
29 ML_SOURCES="$ML_HOME/../src" |
31 |
30 |
32 # Poly/ML 5.3.0 |
31 # Poly/ML 5.4.0 |
33 #ML_PLATFORM=x86-linux |
32 #ML_PLATFORM=x86-linux |
34 #ML_HOME=/usr/local/polyml/x86-linux |
33 #ML_HOME=/usr/local/polyml/x86-linux |
35 #ML_SYSTEM=polyml-5.3.0 |
34 #ML_SYSTEM=polyml-5.4.0 |
36 #ML_OPTIONS="-H 500" |
35 #ML_OPTIONS="-H 500" |
37 #ML_SOURCES="$ML_HOME/../src" |
36 #ML_SOURCES="$ML_HOME/../src" |
38 |
37 |
39 # Poly/ML 5.3.0 (64 bit) |
38 # Poly/ML 5.4.0 (64 bit) |
40 #ML_PLATFORM=x86_64-linux |
39 #ML_PLATFORM=x86_64-linux |
41 #ML_HOME=/usr/local/polyml/x86_64-linux |
40 #ML_HOME=/usr/local/polyml/x86_64-linux |
42 #ML_SYSTEM=polyml-5.3.0 |
41 #ML_SYSTEM=polyml-5.4.0 |
43 #ML_OPTIONS="-H 1000" |
42 #ML_OPTIONS="-H 1000" |
44 #ML_SOURCES="$ML_HOME/../src" |
43 #ML_SOURCES="$ML_HOME/../src" |
45 |
44 |
46 # Standard ML of New Jersey (slow!) |
45 # Standard ML of New Jersey (slow!) |
47 #ML_SYSTEM=smlnj-110 |
46 #ML_SYSTEM=smlnj-110 |