Admin/polyml/settings
author blanchet
Mon, 19 May 2014 23:43:53 +0200
changeset 57005 33f3d2ea803d
parent 56958 b2c2f74d1c93
child 60983 ff4a67c65084
permissions -rw-r--r--
store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
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
53686
432edb1a2469 updated to polyml-5.5.1;
wenzelm
parents: 51060
diff changeset
     3
POLYML_HOME="$COMPONENT"
432edb1a2469 updated to polyml-5.5.1;
wenzelm
parents: 51060
diff changeset
     4
432edb1a2469 updated to polyml-5.5.1;
wenzelm
parents: 51060
diff changeset
     5
49000
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
     6
# basic settings
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
     7
56958
b2c2f74d1c93 updated to polyml-5.5.2;
wenzelm
parents: 53686
diff changeset
     8
#ML_SYSTEM=polyml-5.5.2
53686
432edb1a2469 updated to polyml-5.5.1;
wenzelm
parents: 51060
diff changeset
     9
#ML_PLATFORM="$ISABELLE_PLATFORM32"
432edb1a2469 updated to polyml-5.5.1;
wenzelm
parents: 51060
diff changeset
    10
#ML_HOME="$POLYML_HOME/$ML_PLATFORM"
49000
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    11
#ML_OPTIONS="-H 500"
53686
432edb1a2469 updated to polyml-5.5.1;
wenzelm
parents: 51060
diff changeset
    12
#ML_SOURCES="$POLYML_HOME/src"
49000
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
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    15
# smart settings
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    16
56958
b2c2f74d1c93 updated to polyml-5.5.2;
wenzelm
parents: 53686
diff changeset
    17
ML_SYSTEM=polyml-5.5.2
49000
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    18
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    19
case "$ISABELLE_PLATFORM" in
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    20
  *-linux)
53686
432edb1a2469 updated to polyml-5.5.1;
wenzelm
parents: 51060
diff changeset
    21
    if env LD_LIBRARY_PATH="$POLYML_HOME/$ISABELLE_PLATFORM32:$LD_LIBRARY_PATH" \
432edb1a2469 updated to polyml-5.5.1;
wenzelm
parents: 51060
diff changeset
    22
      "$POLYML_HOME/$ISABELLE_PLATFORM32/poly" -v >/dev/null 2>/dev/null
49000
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    23
    then
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    24
      ML_PLATFORM="$ISABELLE_PLATFORM32"
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    25
    else
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    26
      ML_PLATFORM="$ISABELLE_PLATFORM64"
51060
9effce0ce1e1 tuned ML platform fallback;
wenzelm
parents: 49598
diff changeset
    27
      if [ -z "$ML_PLATFORM_FALLBACK" ]; then
9effce0ce1e1 tuned ML platform fallback;
wenzelm
parents: 49598
diff changeset
    28
        echo >&2 "### Cannot execute Poly/ML in 32bit mode (missing shared libraries for C/C++)"
9effce0ce1e1 tuned ML platform fallback;
wenzelm
parents: 49598
diff changeset
    29
        echo >&2 "### Using bulky 64bit version of Poly/ML instead"
9effce0ce1e1 tuned ML platform fallback;
wenzelm
parents: 49598
diff changeset
    30
        ML_PLATFORM_FALLBACK="true"
9effce0ce1e1 tuned ML platform fallback;
wenzelm
parents: 49598
diff changeset
    31
      fi
49000
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    32
    fi
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    33
    ;;
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    34
  *)
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    35
    ML_PLATFORM="$ISABELLE_PLATFORM32"
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
esac
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
case "$ML_PLATFORM" in
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    40
  x86_64-*)
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    41
    ML_OPTIONS="-H 1000"
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    42
    ;;
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    43
  *)
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    44
    ML_OPTIONS="-H 500"
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    45
    ;;
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    46
esac
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    47
53686
432edb1a2469 updated to polyml-5.5.1;
wenzelm
parents: 51060
diff changeset
    48
ML_HOME="$POLYML_HOME/$ML_PLATFORM"
432edb1a2469 updated to polyml-5.5.1;
wenzelm
parents: 51060
diff changeset
    49
ML_SOURCES="$POLYML_HOME/src"
49000
0cebcbeac4c7 provide polyml-5.4.1 as regular component;
wenzelm
parents:
diff changeset
    50