Admin/polyml/settings
author wenzelm
Tue Nov 07 10:22:10 2017 +0100 (17 months ago)
changeset 67017 ce6454669360
parent 66899 8176914dae84
child 67099 3345d53e7c58
permissions -rw-r--r--
more recent polyml-test version;
afford more heap by default: all platforms are now 64bit and presumably have sufficient memory;
wenzelm@49000
     1
# -*- shell-script -*- :mode=shellscript:
wenzelm@49000
     2
wenzelm@53686
     3
POLYML_HOME="$COMPONENT"
wenzelm@53686
     4
wenzelm@53686
     5
wenzelm@61158
     6
# platform preference
wenzelm@49000
     7
wenzelm@61158
     8
if grep "ML_system_64.*=.*true" "$ISABELLE_HOME_USER/etc/preferences" >/dev/null 2>/dev/null
wenzelm@61158
     9
then
wenzelm@61158
    10
  ML_SYSTEM_64="true"
wenzelm@61158
    11
else
wenzelm@61158
    12
  ML_SYSTEM_64="false"
wenzelm@61158
    13
fi
wenzelm@49000
    14
wenzelm@66761
    15
case "${ISABELLE_PLATFORM_FAMILY}:${ML_SYSTEM_64}" in
wenzelm@66761
    16
  windows:true)
wenzelm@61158
    17
    PLATFORMS="x86_64-windows x86-windows"
wenzelm@49000
    18
    ;;
wenzelm@66761
    19
  windows:*)
wenzelm@61158
    20
    PLATFORMS="x86-windows x86_64-windows"
wenzelm@61158
    21
    ;;
wenzelm@61158
    22
  *:true)
wenzelm@61158
    23
    PLATFORMS="$ISABELLE_PLATFORM64 $ISABELLE_PLATFORM32"
wenzelm@60983
    24
    ;;
wenzelm@49000
    25
  *)
wenzelm@61158
    26
    PLATFORMS="$ISABELLE_PLATFORM32 $ISABELLE_PLATFORM64"
wenzelm@49000
    27
    ;;
wenzelm@49000
    28
esac
wenzelm@49000
    29
wenzelm@61158
    30
wenzelm@61158
    31
# check executable
wenzelm@61158
    32
wenzelm@61158
    33
unset ML_HOME
wenzelm@61158
    34
wenzelm@61158
    35
for PLATFORM in $PLATFORMS
wenzelm@61158
    36
do
wenzelm@61158
    37
  if [ -z "$ML_HOME" ]
wenzelm@61158
    38
  then
wenzelm@64544
    39
    if "$POLYML_HOME/$PLATFORM/polyi" -v </dev/null >/dev/null 2>/dev/null
wenzelm@61158
    40
    then
wenzelm@61158
    41
wenzelm@61158
    42
      # ML settings
wenzelm@61158
    43
wenzelm@66761
    44
      ML_SYSTEM=polyml-5.7.1
wenzelm@61158
    45
      ML_PLATFORM="$PLATFORM"
wenzelm@61158
    46
      ML_HOME="$POLYML_HOME/$ML_PLATFORM"
wenzelm@61158
    47
      ML_SOURCES="$POLYML_HOME/src"
wenzelm@49000
    48
wenzelm@61158
    49
      case "$ML_PLATFORM" in
wenzelm@61158
    50
        x86_64-windows)
wenzelm@66899
    51
          POLYML_EXE="$ML_HOME/poly.exe"
wenzelm@67017
    52
          ML_OPTIONS="--minheap 2000 --codepage utf8"
wenzelm@61158
    53
          ;;
wenzelm@61158
    54
        x86-windows)
wenzelm@66899
    55
          POLYML_EXE="$ML_HOME/poly.exe"
wenzelm@67017
    56
          ML_OPTIONS="--minheap 1000 --codepage utf8"
wenzelm@61158
    57
          ;;
wenzelm@61158
    58
        x86_64-*)
wenzelm@66899
    59
          POLYML_EXE="$ML_HOME/poly"
wenzelm@67017
    60
          ML_OPTIONS="--minheap 2000"
wenzelm@61158
    61
          ;;
wenzelm@61158
    62
        *)
wenzelm@66899
    63
          POLYML_EXE="$ML_HOME/poly"
wenzelm@67017
    64
          ML_OPTIONS="--minheap 1000"
wenzelm@61158
    65
          ;;
wenzelm@61158
    66
      esac
wenzelm@61158
    67
wenzelm@61158
    68
    fi
wenzelm@61158
    69
  fi
wenzelm@61158
    70
done
wenzelm@61158
    71
wenzelm@61158
    72
unset PLATFORM
wenzelm@61158
    73
unset PLATFORMS