Admin/polyml/settings
author wenzelm
Wed, 29 Aug 2012 20:16:22 +0200
changeset 49000 0cebcbeac4c7
child 49400 f0c86a5ef4e2
permissions -rw-r--r--
provide polyml-5.4.1 as regular component; discontinued old-style choosefrom settings with hardwired defaults;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
49000
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
     1
# -*- shell-script -*- :mode=shellscript:
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
     2
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
     3
# basic settings
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
     4
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
     5
#ML_SYSTEM=polyml-5.4.1
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
     6
#ML_PLATFORM="$ISABELLE_PLATFORM"
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
     7
#ML_HOME="$COMPONENT/$ML_PLATFORM"
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
     8
#ML_OPTIONS="-H 500"
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
     9
#ML_SOURCES="$ML_HOME/../src"
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    10
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    11
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    12
# smart settings
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    13
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    14
ML_SYSTEM=polyml-5.4.1
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    15
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    16
case "$ISABELLE_PLATFORM" in
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    17
  *-linux)
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    18
    if env LD_LIBRARY_PATH="$COMPONENT/$ISABELLE_PLATFORM32:$LD_LIBRARY_PATH" \
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    19
      "$COMPONENT/$ISABELLE_PLATFORM32/poly" -v >/dev/null 2>/dev/null
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    20
    then
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    21
      ML_PLATFORM="$ISABELLE_PLATFORM32"
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    22
    else
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    23
      echo >&2 "### Cannot execute Poly/ML in 32bit mode -- using bulky 64bit version instead"
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    24
      ML_PLATFORM="$ISABELLE_PLATFORM64"
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    25
    fi
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    26
    ;;
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    27
  *)
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    28
    ML_PLATFORM="$ISABELLE_PLATFORM32"
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    29
    ;;
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    30
esac
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    31
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    32
case "$ML_PLATFORM" in
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    33
  x86_64-*)
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    34
    ML_OPTIONS="-H 1000"
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    35
    ;;
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    36
  *)
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    37
    ML_OPTIONS="-H 500"
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    38
    ;;
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    39
esac
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    40
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    41
ML_HOME="$COMPONENT/$ML_PLATFORM"
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    42
ML_SOURCES="$COMPONENT/src"
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    43