Admin/polyml/settings

support for explicit scope of private entries;

# -*- 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"