lib/scripts/run-polyml
author wenzelm
Mon Jun 22 15:25:06 1998 +0200 (1998-06-22)
changeset 5063 d45ec8d00ab0
parent 4505 4a2c872b6513
child 8360 885a6414b9c8
permissions -rwxr-xr-x
check_mlhome_file;
wenzelm@3007
     1
#!/bin/bash
wenzelm@2301
     2
#
wenzelm@2314
     3
# $Id$
wenzelm@2314
     4
#
wenzelm@2301
     5
# Poly/ML startup script.
wenzelm@2301
     6
#
wenzelm@4333
     7
# Global vars: INFILE OUTFILE MLTEXT TERMINATE NOWRITE ISABELLE_TMP,
wenzelm@2301
     8
# and from settings
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@5063
    19
function check_mlhome_file()
wenzelm@5063
    20
{
wenzelm@5063
    21
  if [ ! -f "$1" ]; then
wenzelm@5063
    22
    echo "Unable to locate $1" >&2
wenzelm@5063
    23
    echo "Please check your ML_HOME setting!" >&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@2301
    31
POLY=$ML_HOME/poly
wenzelm@2301
    32
DISCGARB=$ML_HOME/discgarb
wenzelm@2301
    33
wenzelm@5063
    34
check_mlhome_file "$POLY"
wenzelm@5063
    35
check_mlhome_file "$DISCGARB"
wenzelm@5063
    36
wenzelm@2301
    37
case "$ML_SYSTEM" in
wenzelm@2349
    38
  polyml-3.*)
wenzelm@2314
    39
    DISCGARB="$DISCGARB -c"
wenzelm@2301
    40
    ;;
wenzelm@2301
    41
esac
wenzelm@2301
    42
wenzelm@2301
    43
wenzelm@2301
    44
## prepare databases
wenzelm@2301
    45
wenzelm@3055
    46
COPYDB=true
wenzelm@2349
    47
wenzelm@2301
    48
if [ -z "$INFILE" ]; then
wenzelm@2400
    49
  INFILE="$ML_HOME/ML_dbase"
wenzelm@5063
    50
  check_mlhome_file "$INFILE"
wenzelm@3055
    51
  MLTEXT="val use = PolyML.use; val exit = PolyML.exit; $MLTEXT"
wenzelm@3055
    52
  COPYDB=""
wenzelm@2301
    53
fi
wenzelm@2301
    54
wenzelm@2301
    55
if [ -z "$OUTFILE" ]; then
wenzelm@2301
    56
  DB="$INFILE"
wenzelm@2349
    57
  ML_OPTIONS="-r $ML_OPTIONS"  
wenzelm@2349
    58
elif [ "$INFILE" -ef "$OUTFILE" ]; then
wenzelm@2301
    59
  DB="$INFILE"
wenzelm@2301
    60
elif [ -n "$COPYDB" ]; then
wenzelm@2936
    61
  [ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out; }
wenzelm@2548
    62
  cp "$INFILE" "$OUTFILE" || fail_out
wenzelm@2349
    63
  chmod +w "$OUTFILE" || fail_out
wenzelm@2301
    64
  DB="$OUTFILE"
wenzelm@2301
    65
else
wenzelm@2936
    66
  [ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out; }
wenzelm@2349
    67
  echo "PolyML.make_database \"$OUTFILE\"; PolyML.quit();" | $POLY -r "$INFILE"
wenzelm@2301
    68
  [ -f "$OUTFILE" ] || fail_out
wenzelm@2301
    69
  DB="$OUTFILE"
wenzelm@2301
    70
fi
wenzelm@2301
    71
wenzelm@2301
    72
wenzelm@2301
    73
## run it!
wenzelm@2301
    74
wenzelm@4505
    75
if [ -z "$TERMINATE" ]; then
wenzelm@4505
    76
  FEEDER_OPTS="-s"
wenzelm@4505
    77
else
wenzelm@4505
    78
  FEEDER_OPTS="-q"
wenzelm@4505
    79
fi
wenzelm@4505
    80
wenzelm@2400
    81
DB_INFO=$(ls -l "$DB")
wenzelm@2349
    82
wenzelm@4505
    83
$ISABELLE_HOME/lib/scripts/feeder -p -h "$MLTEXT" $FEEDER_OPTS | \
wenzelm@4505
    84
  { read FPID; $POLY $ML_OPTIONS "$DB"; RC=$?; kill -HUP $FPID; exit $RC; }
wenzelm@4505
    85
RC=$?
wenzelm@2301
    86
wenzelm@2400
    87
NEW_DB_INFO=$(ls -l "$DB")
wenzelm@2605
    88
[ -n "$OUTFILE" -a "$DB_INFO" != "$NEW_DB_INFO" ] && $DISCGARB "$OUTFILE"
wenzelm@4505
    89
[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
wenzelm@2301
    90
wenzelm@2301
    91
exit $RC