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
     1 # -*- shell-script -*- :mode=shellscript:
     2 
     3 POLYML_HOME="$COMPONENT"
     4 
     5 
     6 # basic settings
     7 
     8 #ML_SYSTEM=polyml-5.5.1
     9 #ML_PLATFORM="$ISABELLE_PLATFORM32"
    10 #ML_HOME="$POLYML_HOME/$ML_PLATFORM"
    11 #ML_OPTIONS="-H 500"
    12 #ML_SOURCES="$POLYML_HOME/src"
    13 
    14 
    15 # smart settings
    16 
    17 ML_SYSTEM=polyml-5.5.1
    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     ;;
    34   *)
    35     ML_PLATFORM="$ISABELLE_PLATFORM32"
    36     ;;
    37 esac
    38 
    39 case "$ML_PLATFORM" in
    40   x86_64-*)
    41     ML_OPTIONS="-H 1000"
    42     ;;
    43   *)
    44     ML_OPTIONS="-H 500"
    45     ;;
    46 esac
    47 
    48 ML_HOME="$POLYML_HOME/$ML_PLATFORM"
    49 ML_SOURCES="$POLYML_HOME/src"
    50