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