lib/scripts/run-mosml
author wenzelm
Mon, 16 Feb 2009 21:23:33 +0100
changeset 29758 7a3b5bbed313
parent 29145 b1c6f4563df7
child 31315 3c7b40548a84
permissions -rwxr-xr-x
removed rudiments of glossary;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10555
2323ec838401 /usr/bin/env bash;
wenzelm
parents: 10105
diff changeset
     1
#!/usr/bin/env bash
9253
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
     2
#
9789
wenzelm
parents: 9253
diff changeset
     3
# Author: Markus Wenzel, TU Muenchen
9253
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
     4
#
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
     5
# Moscow ML 2.00 startup script
9977
32955afeb835 unexport exports;
wenzelm
parents: 9794
diff changeset
     6
10105
f9be78009930 added COPYDB argument;
wenzelm
parents: 9997
diff changeset
     7
export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE
9253
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
     8
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
     9
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    10
## diagnostics
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    11
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    12
function fail_out()
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    13
{
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    14
  echo "Unable to create output heap file: \"$OUTFILE\"" >&2
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    15
  exit 2
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    16
}
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    17
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    18
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    19
## prepare databases
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    20
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    21
MOSML="mosml -P sml90"
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    22
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    23
if [ -z "$INFILE" ]; then
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    24
  EXIT='load "OS"; fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;'
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    25
else
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    26
  EXIT=""
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    27
  echo "Cannot load images yet!" >&2
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    28
  exit 2
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    29
fi
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    30
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    31
if [ -z "$OUTFILE" ]; then
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    32
  COMMIT='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\n"); false);'
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    33
else
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    34
  COMMIT="fun commit () = true;"
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    35
  echo "WARNING: cannot save images yet!" >&2
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    36
  [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    37
fi
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    38
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    39
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    40
## run it!
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    41
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    42
MLTEXT="$EXIT $COMMIT $MLTEXT"
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    43
MLEXIT="commit();"
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    44
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    45
if [ -z "$TERMINATE" ]; then
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    46
  FEEDER_OPTS=""
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    47
else
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    48
  FEEDER_OPTS="-q"
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    49
fi
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    50
9789
wenzelm
parents: 9253
diff changeset
    51
"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
9794
2be239143d42 fixed quoting;
wenzelm
parents: 9789
diff changeset
    52
  { read FPID; "$ML_HOME"/$MOSML $ML_OPTIONS 2>&1; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
9789
wenzelm
parents: 9253
diff changeset
    53
RC="$?"
9253
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    54
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    55
[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    56
9789
wenzelm
parents: 9253
diff changeset
    57
exit "$RC"