Admin/polyml/settings
author haftmann
Sun Dec 15 15:10:16 2013 +0100 (2013-12-15)
changeset 54745 46e441e61ff5
parent 53686 432edb1a2469
child 56958 b2c2f74d1c93
permissions -rw-r--r--
disambiguation of interpretation prefixes
wenzelm@49000
     1
# -*- shell-script -*- :mode=shellscript:
wenzelm@49000
     2
wenzelm@53686
     3
POLYML_HOME="$COMPONENT"
wenzelm@53686
     4
wenzelm@53686
     5
wenzelm@49000
     6
# basic settings
wenzelm@49000
     7
wenzelm@53686
     8
#ML_SYSTEM=polyml-5.5.1
wenzelm@53686
     9
#ML_PLATFORM="$ISABELLE_PLATFORM32"
wenzelm@53686
    10
#ML_HOME="$POLYML_HOME/$ML_PLATFORM"
wenzelm@49000
    11
#ML_OPTIONS="-H 500"
wenzelm@53686
    12
#ML_SOURCES="$POLYML_HOME/src"
wenzelm@49000
    13
wenzelm@49000
    14
wenzelm@49000
    15
# smart settings
wenzelm@49000
    16
wenzelm@53686
    17
ML_SYSTEM=polyml-5.5.1
wenzelm@49000
    18
wenzelm@49000
    19
case "$ISABELLE_PLATFORM" in
wenzelm@49000
    20
  *-linux)
wenzelm@53686
    21
    if env LD_LIBRARY_PATH="$POLYML_HOME/$ISABELLE_PLATFORM32:$LD_LIBRARY_PATH" \
wenzelm@53686
    22
      "$POLYML_HOME/$ISABELLE_PLATFORM32/poly" -v >/dev/null 2>/dev/null
wenzelm@49000
    23
    then
wenzelm@49000
    24
      ML_PLATFORM="$ISABELLE_PLATFORM32"
wenzelm@49000
    25
    else
wenzelm@49000
    26
      ML_PLATFORM="$ISABELLE_PLATFORM64"
wenzelm@51060
    27
      if [ -z "$ML_PLATFORM_FALLBACK" ]; then
wenzelm@51060
    28
        echo >&2 "### Cannot execute Poly/ML in 32bit mode (missing shared libraries for C/C++)"
wenzelm@51060
    29
        echo >&2 "### Using bulky 64bit version of Poly/ML instead"
wenzelm@51060
    30
        ML_PLATFORM_FALLBACK="true"
wenzelm@51060
    31
      fi
wenzelm@49000
    32
    fi
wenzelm@49000
    33
    ;;
wenzelm@49000
    34
  *)
wenzelm@49000
    35
    ML_PLATFORM="$ISABELLE_PLATFORM32"
wenzelm@49000
    36
    ;;
wenzelm@49000
    37
esac
wenzelm@49000
    38
wenzelm@49000
    39
case "$ML_PLATFORM" in
wenzelm@49000
    40
  x86_64-*)
wenzelm@49000
    41
    ML_OPTIONS="-H 1000"
wenzelm@49000
    42
    ;;
wenzelm@49000
    43
  *)
wenzelm@49000
    44
    ML_OPTIONS="-H 500"
wenzelm@49000
    45
    ;;
wenzelm@49000
    46
esac
wenzelm@49000
    47
wenzelm@53686
    48
ML_HOME="$POLYML_HOME/$ML_PLATFORM"
wenzelm@53686
    49
ML_SOURCES="$POLYML_HOME/src"
wenzelm@49000
    50