Admin/polyml/settings
author blanchet
Mon, 19 May 2014 23:43:53 +0200
changeset 57005 33f3d2ea803d
parent 56958 b2c2f74d1c93
child 60983 ff4a67c65084
permissions -rw-r--r--
store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution

# -*- shell-script -*- :mode=shellscript:

POLYML_HOME="$COMPONENT"


# basic settings

#ML_SYSTEM=polyml-5.5.2
#ML_PLATFORM="$ISABELLE_PLATFORM32"
#ML_HOME="$POLYML_HOME/$ML_PLATFORM"
#ML_OPTIONS="-H 500"
#ML_SOURCES="$POLYML_HOME/src"


# smart settings

ML_SYSTEM=polyml-5.5.2

case "$ISABELLE_PLATFORM" in
  *-linux)
    if env LD_LIBRARY_PATH="$POLYML_HOME/$ISABELLE_PLATFORM32:$LD_LIBRARY_PATH" \
      "$POLYML_HOME/$ISABELLE_PLATFORM32/poly" -v >/dev/null 2>/dev/null
    then
      ML_PLATFORM="$ISABELLE_PLATFORM32"
    else
      ML_PLATFORM="$ISABELLE_PLATFORM64"
      if [ -z "$ML_PLATFORM_FALLBACK" ]; then
        echo >&2 "### Cannot execute Poly/ML in 32bit mode (missing shared libraries for C/C++)"
        echo >&2 "### Using bulky 64bit version of Poly/ML instead"
        ML_PLATFORM_FALLBACK="true"
      fi
    fi
    ;;
  *)
    ML_PLATFORM="$ISABELLE_PLATFORM32"
    ;;
esac

case "$ML_PLATFORM" in
  x86_64-*)
    ML_OPTIONS="-H 1000"
    ;;
  *)
    ML_OPTIONS="-H 500"
    ;;
esac

ML_HOME="$POLYML_HOME/$ML_PLATFORM"
ML_SOURCES="$POLYML_HOME/src"