lib/scripts/run-polyml
author wenzelm
Sat Jun 11 23:17:28 2005 +0200 (2005-06-11)
changeset 16374 f4b7cf8975af
parent 16285 75954ae8b247
child 16392 7212040b71f2
permissions -rwxr-xr-x
some cygwin support;
wenzelm@10555
     1
#!/usr/bin/env bash
wenzelm@2301
     2
#
wenzelm@2314
     3
# $Id$
wenzelm@9789
     4
# Author: Markus Wenzel, TU Muenchen
wenzelm@2314
     5
#
wenzelm@2301
     6
# Poly/ML startup script.
wenzelm@9977
     7
wenzelm@10105
     8
export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE
wenzelm@2301
     9
wenzelm@2301
    10
wenzelm@2301
    11
## diagnostics
wenzelm@2301
    12
wenzelm@2349
    13
function fail_out()
wenzelm@2301
    14
{
wenzelm@2349
    15
  echo "Unable to create output heap file: \"$OUTFILE\"" >&2
wenzelm@2301
    16
  exit 2
wenzelm@2301
    17
}
wenzelm@2301
    18
wenzelm@10206
    19
function check_file()
wenzelm@5063
    20
{
wenzelm@5063
    21
  if [ ! -f "$1" ]; then
wenzelm@5063
    22
    echo "Unable to locate $1" >&2
wenzelm@10206
    23
    echo "Please check your ML system settings!" >&2
wenzelm@5063
    24
    exit 2
wenzelm@5063
    25
  fi
wenzelm@5063
    26
}
wenzelm@5063
    27
wenzelm@2301
    28
wenzelm@2400
    29
## Poly/ML programs
wenzelm@2301
    30
wenzelm@10206
    31
ML_DBASE_PREFIX=""
wenzelm@16374
    32
ML_DBASE_SUFFIX=""
wenzelm@16374
    33
CYGPATH=""
wenzelm@16374
    34
wenzelm@16374
    35
case "$ML_PLATFORM" in
wenzelm@16374
    36
  *-cygwin)
wenzelm@16374
    37
    ML_DBASE_SUFFIX=".pmd"
wenzelm@16374
    38
    POLY="$ML_HOME/PolyML.exe"
wenzelm@16374
    39
    CYGPATH="cygpath -m"
wenzelm@16374
    40
    ;;
wenzelm@16374
    41
  *)
wenzelm@16374
    42
    POLY="$ML_HOME/poly"
wenzelm@16374
    43
    ;;
wenzelm@16374
    44
esac
wenzelm@16374
    45
wenzelm@10206
    46
check_file "$POLY"
wenzelm@2301
    47
wenzelm@9765
    48
case "$ML_SYSTEM" in
wenzelm@9765
    49
  polyml-4.*)
wenzelm@10206
    50
    if [ -z "$ML_DBASE" ]; then
wenzelm@10206
    51
      if [ -z "$COPYDB" ]; then
wenzelm@10206
    52
        ML_DBASE_PREFIX="$ML_HOME/"
wenzelm@16374
    53
        ML_DBASE="ML_dbase${ML_DBASE_SUFFIX}"
wenzelm@10206
    54
      else
wenzelm@16374
    55
        ML_DBASE="$ML_HOME/ML_dbase${ML_DBASE_SUFFIX}"
wenzelm@10206
    56
      fi
wenzelm@10206
    57
      POLYPATH="$ML_HOME"
wenzelm@10206
    58
    else
wenzelm@16374
    59
      POLYPATH="$(dirname "$ML_DBASE")"
wenzelm@10206
    60
    fi
wenzelm@10206
    61
    export POLYPATH
wenzelm@10206
    62
wenzelm@10206
    63
    DISCGARB="$POLY"
wenzelm@10206
    64
    DISCGARB_OPTIONS="-d -c"
wenzelm@10206
    65
wenzelm@9765
    66
    EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;"
wenzelm@9765
    67
    ;;
wenzelm@9765
    68
  *)
wenzelm@10206
    69
    if [ -z "$ML_DBASE" ]; then
wenzelm@10206
    70
      ML_DBASE="$ML_HOME/ML_dbase"
wenzelm@10206
    71
    fi
wenzelm@10206
    72
wenzelm@10206
    73
    DISCGARB="$ML_HOME/discgarb"
wenzelm@10206
    74
    DISCGARB_OPTIONS="-c"
wenzelm@10206
    75
    check_file "$DISCGARB"
wenzelm@10206
    76
wenzelm@9765
    77
    EXIT="val exit = PolyML.exit;"
wenzelm@9765
    78
    ;;
wenzelm@9765
    79
esac
wenzelm@9765
    80
wenzelm@9765
    81
wenzelm@2301
    82
## prepare databases
wenzelm@2301
    83
wenzelm@2301
    84
if [ -z "$INFILE" ]; then
wenzelm@10206
    85
  check_file "$ML_DBASE_PREFIX$ML_DBASE"
wenzelm@10206
    86
  INFILE="$ML_DBASE"
wenzelm@9765
    87
  MLTEXT="val use = PolyML.use; $EXIT $MLTEXT"
wenzelm@16285
    88
  case "$ML_SYSTEM" in
wenzelm@16285
    89
    polyml-4.1.[12])
wenzelm@16285
    90
      DISCGARB_OPTIONS="$DISCGARB_OPTIONS -S 180"
wenzelm@16285
    91
      ;;
wenzelm@16285
    92
    polyml-4.1.*)
wenzelm@16285
    93
      DISCGARB_OPTIONS="$DISCGARB_OPTIONS -S max"
wenzelm@16285
    94
      ;;
wenzelm@16285
    95
  esac
wenzelm@10105
    96
else
wenzelm@10105
    97
  COPYDB=true
wenzelm@2301
    98
fi
wenzelm@2301
    99
wenzelm@2301
   100
if [ -z "$OUTFILE" ]; then
wenzelm@2301
   101
  DB="$INFILE"
wenzelm@15850
   102
  ML_OPTIONS="-r $ML_OPTIONS"
wenzelm@2349
   103
elif [ "$INFILE" -ef "$OUTFILE" ]; then
wenzelm@2301
   104
  DB="$INFILE"
wenzelm@2301
   105
elif [ -n "$COPYDB" ]; then
wenzelm@2936
   106
  [ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out; }
wenzelm@2548
   107
  cp "$INFILE" "$OUTFILE" || fail_out
wenzelm@2349
   108
  chmod +w "$OUTFILE" || fail_out
wenzelm@2301
   109
  DB="$OUTFILE"
wenzelm@2301
   110
else
wenzelm@2936
   111
  [ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out; }
wenzelm@16374
   112
  if [ -z "$CYGPATH" ]; then
wenzelm@16374
   113
    echo "PolyML.make_database \"$OUTFILE\"; PolyML.quit();" | "$POLY" -r "$INFILE"
wenzelm@16374
   114
  else
wenzelm@16374
   115
    OUTFILE_CYGWIN="$($CYGPATH "$OUTFILE")"
wenzelm@16374
   116
    INFILE_CYGWIN="$($CYGPATH "$INFILE")"
wenzelm@16374
   117
    echo "PolyML.make_database \"$OUTFILE_CYGWIN\"; PolyML.quit();" | "$POLY" -r "$INFILE_CYGWIN"
wenzelm@16374
   118
  fi
wenzelm@2301
   119
  [ -f "$OUTFILE" ] || fail_out
wenzelm@2301
   120
  DB="$OUTFILE"
wenzelm@2301
   121
fi
wenzelm@2301
   122
wenzelm@2301
   123
wenzelm@2301
   124
## run it!
wenzelm@2301
   125
wenzelm@16254
   126
if [ -z "$TERMINATE" ]; then
wenzelm@16254
   127
  FEEDER_OPTS=""
wenzelm@16254
   128
else
wenzelm@16254
   129
  FEEDER_OPTS="-q"
wenzelm@16254
   130
fi
wenzelm@16254
   131
wenzelm@15850
   132
DB_INFO=$(ls -l "$DB" 2>/dev/null)
wenzelm@15850
   133
wenzelm@16374
   134
if [ -z "$CYGPATH" ]; then
wenzelm@16374
   135
  "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" $FEEDER_OPTS | \
wenzelm@16374
   136
    { read FPID; "$POLY" $ML_OPTIONS "$DB"; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
wenzelm@16374
   137
else
wenzelm@16374
   138
  DB_CYGWIN="$($CYGPATH "$DB")"
wenzelm@16374
   139
  "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" $FEEDER_OPTS | \
wenzelm@16374
   140
    { read FPID; "$POLY" $ML_OPTIONS "$DB_CYGWIN"; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
wenzelm@16374
   141
fi
wenzelm@9789
   142
RC="$?"
wenzelm@2301
   143
wenzelm@10206
   144
NEW_DB_INFO=$(ls -l "$DB" 2>/dev/null)
wenzelm@10206
   145
[ -n "$OUTFILE" -a -n "$COMPRESS" -a "$DB_INFO" != "$NEW_DB_INFO" ] && \
wenzelm@10206
   146
  "$DISCGARB" $DISCGARB_OPTIONS "$OUTFILE"
wenzelm@4505
   147
[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
wenzelm@2301
   148
wenzelm@9789
   149
exit "$RC"