Admin/polyml/settings
author wenzelm
Sat, 26 Jan 2013 19:52:49 +0100
changeset 51060 9effce0ce1e1
parent 49598 7bc5fcc03564
child 53686 432edb1a2469
permissions -rw-r--r--
tuned ML platform fallback;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
49000
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
     1
# -*- shell-script -*- :mode=shellscript:
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
     2
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
     3
# basic settings
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
     4
49400
f0c86a5ef4e2 some updates for polyml-5.5.0;
wenzelm
parents: 49000
diff changeset
     5
#ML_SYSTEM=polyml-5.5.0
49000
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
     6
#ML_PLATFORM="$ISABELLE_PLATFORM"
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
     7
#ML_HOME="$COMPONENT/$ML_PLATFORM"
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
     8
#ML_OPTIONS="-H 500"
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
     9
#ML_SOURCES="$ML_HOME/../src"
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    10
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    11
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    12
# smart settings
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    13
49400
f0c86a5ef4e2 some updates for polyml-5.5.0;
wenzelm
parents: 49000
diff changeset
    14
ML_SYSTEM=polyml-5.5.0
49000
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    15
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    16
case "$ISABELLE_PLATFORM" in
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    17
  *-linux)
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    18
    if env LD_LIBRARY_PATH="$COMPONENT/$ISABELLE_PLATFORM32:$LD_LIBRARY_PATH" \
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    19
      "$COMPONENT/$ISABELLE_PLATFORM32/poly" -v >/dev/null 2>/dev/null
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    20
    then
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    21
      ML_PLATFORM="$ISABELLE_PLATFORM32"
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    22
    else
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    23
      ML_PLATFORM="$ISABELLE_PLATFORM64"
51060
9effce0ce1e1 tuned ML platform fallback;
wenzelm
parents: 49598
diff changeset
    24
      if [ -z "$ML_PLATFORM_FALLBACK" ]; then
9effce0ce1e1 tuned ML platform fallback;
wenzelm
parents: 49598
diff changeset
    25
        echo >&2 "### Cannot execute Poly/ML in 32bit mode (missing shared libraries for C/C++)"
9effce0ce1e1 tuned ML platform fallback;
wenzelm
parents: 49598
diff changeset
    26
        echo >&2 "### Using bulky 64bit version of Poly/ML instead"
9effce0ce1e1 tuned ML platform fallback;
wenzelm
parents: 49598
diff changeset
    27
        ML_PLATFORM_FALLBACK="true"
9effce0ce1e1 tuned ML platform fallback;
wenzelm
parents: 49598
diff changeset
    28
      fi
49000
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    29
    fi
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    30
    ;;
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    31
  *)
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    32
    ML_PLATFORM="$ISABELLE_PLATFORM32"
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    33
    ;;
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    34
esac
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    35
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    36
case "$ML_PLATFORM" in
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    37
  x86_64-*)
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    38
    ML_OPTIONS="-H 1000"
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    39
    ;;
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    40
  *)
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    41
    ML_OPTIONS="-H 500"
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    42
    ;;
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    43
esac
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    44
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    45
ML_HOME="$COMPONENT/$ML_PLATFORM"
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    46
ML_SOURCES="$COMPONENT/src"
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    47