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

POLYML_HOME="$COMPONENT"

# basic settings

#ML_SYSTEM=polyml-5.5.1

#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.1

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"