Admin/polyml/settings
author wenzelm
Wed, 26 Sep 2012 16:37:21 +0200
changeset 49598 7bc5fcc03564
parent 49400 f0c86a5ef4e2
child 51060 9effce0ce1e1
permissions -rw-r--r--
tuned message;
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
49400
f0c86a5ef4e2 some updates for polyml-5.5.0;
wenzelm
parents: 49000
diff changeset
     5
#ML_SYSTEM=polyml-5.5.0
49000
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
49400
f0c86a5ef4e2 some updates for polyml-5.5.0;
wenzelm
parents: 49000
diff changeset
    14
ML_SYSTEM=polyml-5.5.0
49000
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
49598
7bc5fcc03564 tuned message;
wenzelm
parents: 49400
diff changeset
    23
      echo >&2 "### Cannot execute Poly/ML in 32bit mode: missing shared libraries for C/C++"
7bc5fcc03564 tuned message;
wenzelm
parents: 49400
diff changeset
    24
      echo >&2 "### Using more voluminous 64bit version of Poly/ML instead"
49000
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    25
      ML_PLATFORM="$ISABELLE_PLATFORM64"
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    26
    fi
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
  *)
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    29
    ML_PLATFORM="$ISABELLE_PLATFORM32"
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    30
    ;;
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    31
esac
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    32
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    33
case "$ML_PLATFORM" in
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    34
  x86_64-*)
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    35
    ML_OPTIONS="-H 1000"
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
  *)
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    38
    ML_OPTIONS="-H 500"
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    39
    ;;
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    40
esac
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    41
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    42
ML_HOME="$COMPONENT/$ML_PLATFORM"
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    43
ML_SOURCES="$COMPONENT/src"
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    44