lib/scripts/run-polyml
author wenzelm
Thu Oct 12 17:48:06 2000 +0200 (2000-10-12)
changeset 10206 d48a2e324abf
parent 10105 f9be78009930
child 10555 2323ec838401
permissions -rwxr-xr-x
accomodate Poly/ML 4.0;
wenzelm@3007
     1
#!/bin/bash
wenzelm@2301
     2
#
wenzelm@2314
     3
# $Id$
wenzelm@9789
     4
# Author: Markus Wenzel, TU Muenchen
wenzelm@9789
     5
# License: GPL (GNU GENERAL PUBLIC LICENSE)
wenzelm@2314
     6
#
wenzelm@2301
     7
# Poly/ML startup script.
wenzelm@9977
     8
wenzelm@10105
     9
export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE
wenzelm@2301
    10
wenzelm@2301
    11
wenzelm@2301
    12
## diagnostics
wenzelm@2301
    13
wenzelm@2349
    14
function fail_out()
wenzelm@2301
    15
{
wenzelm@2349
    16
  echo "Unable to create output heap file: \"$OUTFILE\"" >&2
wenzelm@2301
    17
  exit 2
wenzelm@2301
    18
}
wenzelm@2301
    19
wenzelm@10206
    20
function check_file()
wenzelm@5063
    21
{
wenzelm@5063
    22
  if [ ! -f "$1" ]; then
wenzelm@5063
    23
    echo "Unable to locate $1" >&2
wenzelm@10206
    24
    echo "Please check your ML system settings!" >&2
wenzelm@5063
    25
    exit 2
wenzelm@5063
    26
  fi
wenzelm@5063
    27
}
wenzelm@5063
    28
wenzelm@2301
    29
wenzelm@2400
    30
## Poly/ML programs
wenzelm@2301
    31
wenzelm@10206
    32
ML_DBASE_PREFIX=""
wenzelm@9789
    33
POLY="$ML_HOME/poly"
wenzelm@10206
    34
check_file "$POLY"
wenzelm@2301
    35
wenzelm@9765
    36
case "$ML_SYSTEM" in
wenzelm@9765
    37
  polyml-4.*)
wenzelm@10206
    38
    if [ -z "$ML_DBASE" ]; then
wenzelm@10206
    39
      if [ -z "$COPYDB" ]; then
wenzelm@10206
    40
        ML_DBASE_PREFIX="$ML_HOME/"
wenzelm@10206
    41
        ML_DBASE="ML_dbase"
wenzelm@10206
    42
      else
wenzelm@10206
    43
        ML_DBASE="$ML_HOME/ML_dbase"
wenzelm@10206
    44
      fi
wenzelm@10206
    45
      POLYPATH="$ML_HOME"
wenzelm@10206
    46
    else
wenzelm@10206
    47
      POLYPATH=$(dirname "$ML_DBASE")
wenzelm@10206
    48
    fi
wenzelm@10206
    49
    export POLYPATH
wenzelm@10206
    50
wenzelm@10206
    51
    DISCGARB="$POLY"
wenzelm@10206
    52
    DISCGARB_OPTIONS="-d -c"
wenzelm@10206
    53
wenzelm@9765
    54
    EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;"
wenzelm@9765
    55
    ;;
wenzelm@9765
    56
  *)
wenzelm@10206
    57
    if [ -z "$ML_DBASE" ]; then
wenzelm@10206
    58
      ML_DBASE="$ML_HOME/ML_dbase"
wenzelm@10206
    59
    fi
wenzelm@10206
    60
wenzelm@10206
    61
    DISCGARB="$ML_HOME/discgarb"
wenzelm@10206
    62
    DISCGARB_OPTIONS="-c"
wenzelm@10206
    63
    check_file "$DISCGARB"
wenzelm@10206
    64
wenzelm@9765
    65
    EXIT="val exit = PolyML.exit;"
wenzelm@9765
    66
    ;;
wenzelm@9765
    67
esac
wenzelm@9765
    68
wenzelm@9765
    69
wenzelm@2301
    70
## prepare databases
wenzelm@2301
    71
wenzelm@2301
    72
if [ -z "$INFILE" ]; then
wenzelm@10206
    73
  check_file "$ML_DBASE_PREFIX$ML_DBASE"
wenzelm@10206
    74
  INFILE="$ML_DBASE"
wenzelm@9765
    75
  MLTEXT="val use = PolyML.use; $EXIT $MLTEXT"
wenzelm@10105
    76
else
wenzelm@10105
    77
  COPYDB=true
wenzelm@2301
    78
fi
wenzelm@2301
    79
wenzelm@2301
    80
if [ -z "$OUTFILE" ]; then
wenzelm@2301
    81
  DB="$INFILE"
wenzelm@2349
    82
  ML_OPTIONS="-r $ML_OPTIONS"  
wenzelm@2349
    83
elif [ "$INFILE" -ef "$OUTFILE" ]; then
wenzelm@2301
    84
  DB="$INFILE"
wenzelm@2301
    85
elif [ -n "$COPYDB" ]; then
wenzelm@2936
    86
  [ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out; }
wenzelm@2548
    87
  cp "$INFILE" "$OUTFILE" || fail_out
wenzelm@2349
    88
  chmod +w "$OUTFILE" || fail_out
wenzelm@2301
    89
  DB="$OUTFILE"
wenzelm@2301
    90
else
wenzelm@2936
    91
  [ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out; }
wenzelm@9789
    92
  echo "PolyML.make_database \"$OUTFILE\"; PolyML.quit();" | "$POLY" -r "$INFILE"
wenzelm@2301
    93
  [ -f "$OUTFILE" ] || fail_out
wenzelm@2301
    94
  DB="$OUTFILE"
wenzelm@2301
    95
fi
wenzelm@2301
    96
wenzelm@2301
    97
wenzelm@2301
    98
## run it!
wenzelm@2301
    99
wenzelm@4505
   100
if [ -z "$TERMINATE" ]; then
wenzelm@4505
   101
  FEEDER_OPTS="-s"
wenzelm@4505
   102
else
wenzelm@4505
   103
  FEEDER_OPTS="-q"
wenzelm@4505
   104
fi
wenzelm@4505
   105
wenzelm@10206
   106
DB_INFO=$(ls -l "$DB" 2>/dev/null)
wenzelm@2349
   107
wenzelm@9789
   108
"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" $FEEDER_OPTS | \
wenzelm@9789
   109
  { read FPID; "$POLY" $ML_OPTIONS "$DB"; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
wenzelm@9789
   110
RC="$?"
wenzelm@2301
   111
wenzelm@10206
   112
NEW_DB_INFO=$(ls -l "$DB" 2>/dev/null)
wenzelm@10206
   113
[ -n "$OUTFILE" -a -n "$COMPRESS" -a "$DB_INFO" != "$NEW_DB_INFO" ] && \
wenzelm@10206
   114
  "$DISCGARB" $DISCGARB_OPTIONS "$OUTFILE"
wenzelm@4505
   115
[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
wenzelm@2301
   116
wenzelm@9789
   117
exit "$RC"