lib/scripts/run-polyml
author wenzelm
Sun Jun 05 11:31:17 2005 +0200 (2005-06-05)
changeset 16254 1b2683e18fd2
parent 15850 30e878979457
child 16285 75954ae8b247
permissions -rwxr-xr-x
DISCGARB_OPTIONS: proper treatment of specific polyml versions;
the feeder is back (previous version did not really work with Isar.loop);
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@9789
    32
POLY="$ML_HOME/poly"
wenzelm@10206
    33
check_file "$POLY"
wenzelm@2301
    34
wenzelm@9765
    35
case "$ML_SYSTEM" in
wenzelm@9765
    36
  polyml-4.*)
wenzelm@10206
    37
    if [ -z "$ML_DBASE" ]; then
wenzelm@10206
    38
      if [ -z "$COPYDB" ]; then
wenzelm@10206
    39
        ML_DBASE_PREFIX="$ML_HOME/"
wenzelm@10206
    40
        ML_DBASE="ML_dbase"
wenzelm@10206
    41
      else
wenzelm@10206
    42
        ML_DBASE="$ML_HOME/ML_dbase"
wenzelm@10206
    43
      fi
wenzelm@10206
    44
      POLYPATH="$ML_HOME"
wenzelm@10206
    45
    else
wenzelm@10206
    46
      POLYPATH=$(dirname "$ML_DBASE")
wenzelm@10206
    47
    fi
wenzelm@10206
    48
    export POLYPATH
wenzelm@10206
    49
wenzelm@10206
    50
    DISCGARB="$POLY"
wenzelm@10206
    51
    DISCGARB_OPTIONS="-d -c"
wenzelm@16254
    52
    case "$ML_SYSTEM" in
wenzelm@16254
    53
      polyml-4.1.[12])
wenzelm@16254
    54
	DISCGARB_OPTIONS="$DISCGARB_OPTIONS -S 180"
wenzelm@16254
    55
	;;
wenzelm@16254
    56
      polyml-4.1.*)
wenzelm@16254
    57
	DISCGARB_OPTIONS="$DISCGARB_OPTIONS -S max"
wenzelm@16254
    58
	;;
wenzelm@16254
    59
    esac
wenzelm@10206
    60
wenzelm@9765
    61
    EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;"
wenzelm@9765
    62
    ;;
wenzelm@9765
    63
  *)
wenzelm@10206
    64
    if [ -z "$ML_DBASE" ]; then
wenzelm@10206
    65
      ML_DBASE="$ML_HOME/ML_dbase"
wenzelm@10206
    66
    fi
wenzelm@10206
    67
wenzelm@10206
    68
    DISCGARB="$ML_HOME/discgarb"
wenzelm@10206
    69
    DISCGARB_OPTIONS="-c"
wenzelm@10206
    70
    check_file "$DISCGARB"
wenzelm@10206
    71
wenzelm@9765
    72
    EXIT="val exit = PolyML.exit;"
wenzelm@9765
    73
    ;;
wenzelm@9765
    74
esac
wenzelm@9765
    75
wenzelm@9765
    76
wenzelm@2301
    77
## prepare databases
wenzelm@2301
    78
wenzelm@2301
    79
if [ -z "$INFILE" ]; then
wenzelm@10206
    80
  check_file "$ML_DBASE_PREFIX$ML_DBASE"
wenzelm@10206
    81
  INFILE="$ML_DBASE"
wenzelm@9765
    82
  MLTEXT="val use = PolyML.use; $EXIT $MLTEXT"
wenzelm@10105
    83
else
wenzelm@10105
    84
  COPYDB=true
wenzelm@2301
    85
fi
wenzelm@2301
    86
wenzelm@2301
    87
if [ -z "$OUTFILE" ]; then
wenzelm@2301
    88
  DB="$INFILE"
wenzelm@15850
    89
  ML_OPTIONS="-r $ML_OPTIONS"
wenzelm@2349
    90
elif [ "$INFILE" -ef "$OUTFILE" ]; then
wenzelm@2301
    91
  DB="$INFILE"
wenzelm@2301
    92
elif [ -n "$COPYDB" ]; then
wenzelm@2936
    93
  [ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out; }
wenzelm@2548
    94
  cp "$INFILE" "$OUTFILE" || fail_out
wenzelm@2349
    95
  chmod +w "$OUTFILE" || fail_out
wenzelm@2301
    96
  DB="$OUTFILE"
wenzelm@2301
    97
else
wenzelm@2936
    98
  [ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out; }
wenzelm@9789
    99
  echo "PolyML.make_database \"$OUTFILE\"; PolyML.quit();" | "$POLY" -r "$INFILE"
wenzelm@2301
   100
  [ -f "$OUTFILE" ] || fail_out
wenzelm@2301
   101
  DB="$OUTFILE"
wenzelm@2301
   102
fi
wenzelm@2301
   103
wenzelm@2301
   104
wenzelm@2301
   105
## run it!
wenzelm@2301
   106
wenzelm@16254
   107
if [ -z "$TERMINATE" ]; then
wenzelm@16254
   108
  FEEDER_OPTS=""
wenzelm@16254
   109
else
wenzelm@16254
   110
  FEEDER_OPTS="-q"
wenzelm@16254
   111
fi
wenzelm@16254
   112
wenzelm@15850
   113
DB_INFO=$(ls -l "$DB" 2>/dev/null)
wenzelm@15850
   114
wenzelm@16254
   115
"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" $FEEDER_OPTS | \
wenzelm@16254
   116
  { read FPID; "$POLY" $ML_OPTIONS "$DB"; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
wenzelm@9789
   117
RC="$?"
wenzelm@2301
   118
wenzelm@10206
   119
NEW_DB_INFO=$(ls -l "$DB" 2>/dev/null)
wenzelm@10206
   120
[ -n "$OUTFILE" -a -n "$COMPRESS" -a "$DB_INFO" != "$NEW_DB_INFO" ] && \
wenzelm@10206
   121
  "$DISCGARB" $DISCGARB_OPTIONS "$OUTFILE"
wenzelm@4505
   122
[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
wenzelm@2301
   123
wenzelm@9789
   124
exit "$RC"