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;
     1 # -*- shell-script -*- :mode=shellscript:
     2 
     3 POLYML_HOME="$COMPONENT"
     4 
     5 
     6 # platform preference
     7 
     8 if grep "ML_system_64.*=.*true" "$ISABELLE_HOME_USER/etc/preferences" >/dev/null 2>/dev/null
     9 then
    10   ML_SYSTEM_64="true"
    11 else
    12   ML_SYSTEM_64="false"
    13 fi
    14 
    15 case "${ISABELLE_PLATFORM_FAMILY}:${ML_SYSTEM_64}" in
    16   windows:true)
    17     PLATFORMS="x86_64-windows x86-windows"
    18     ;;
    19   windows:*)
    20     PLATFORMS="x86-windows x86_64-windows"
    21     ;;
    22   *:true)
    23     PLATFORMS="$ISABELLE_PLATFORM64 $ISABELLE_PLATFORM32"
    24     ;;
    25   *)
    26     PLATFORMS="$ISABELLE_PLATFORM32 $ISABELLE_PLATFORM64"
    27     ;;
    28 esac
    29 
    30 
    31 # check executable
    32 
    33 unset ML_HOME
    34 
    35 for PLATFORM in $PLATFORMS
    36 do
    37   if [ -z "$ML_HOME" ]
    38   then
    39     if "$POLYML_HOME/$PLATFORM/polyi" -v </dev/null >/dev/null 2>/dev/null
    40     then
    41 
    42       # ML settings
    43 
    44       ML_SYSTEM=polyml-5.7.1
    45       ML_PLATFORM="$PLATFORM"
    46       ML_HOME="$POLYML_HOME/$ML_PLATFORM"
    47       ML_SOURCES="$POLYML_HOME/src"
    48 
    49       case "$ML_PLATFORM" in
    50         x86_64-windows)
    51           POLYML_EXE="$ML_HOME/poly.exe"
    52           ML_OPTIONS="--minheap 2000 --codepage utf8"
    53           ;;
    54         x86-windows)
    55           POLYML_EXE="$ML_HOME/poly.exe"
    56           ML_OPTIONS="--minheap 1000 --codepage utf8"
    57           ;;
    58         x86_64-*)
    59           POLYML_EXE="$ML_HOME/poly"
    60           ML_OPTIONS="--minheap 2000"
    61           ;;
    62         *)
    63           POLYML_EXE="$ML_HOME/poly"
    64           ML_OPTIONS="--minheap 1000"
    65           ;;
    66       esac
    67 
    68     fi
    69   fi
    70 done
    71 
    72 unset PLATFORM
    73 unset PLATFORMS