lib/scripts/run-mosml
author wenzelm
Wed, 26 Jul 2006 00:44:44 +0200
changeset 20207 4c57e850e8d5
parent 14981 e73f8140af78
child 29145 b1c6f4563df7
permissions -rwxr-xr-x
added Pure/subgoal.ML;
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
#
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
     3
# $Id$
9789
wenzelm
parents: 9253
diff changeset
     4
# Author: Markus Wenzel, TU Muenchen
9253
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
     5
#
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
     6
# Moscow ML 2.00 startup script
9977
32955afeb835 unexport exports;
wenzelm
parents: 9794
diff changeset
     7
10105
f9be78009930 added COPYDB argument;
wenzelm
parents: 9997
diff changeset
     8
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
     9
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    10
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    11
## diagnostics
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    12
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    13
function fail_out()
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    14
{
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    15
  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
    16
  exit 2
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
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    20
## prepare databases
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    21
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    22
MOSML="mosml -P sml90"
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    23
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    24
if [ -z "$INFILE" ]; then
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    25
  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
    26
else
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    27
  EXIT=""
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    28
  echo "Cannot load images yet!" >&2
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    29
  exit 2
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    30
fi
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    31
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    32
if [ -z "$OUTFILE" ]; then
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    33
  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
    34
else
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    35
  COMMIT="fun commit () = true;"
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    36
  echo "WARNING: cannot save images yet!" >&2
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    37
  [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    38
fi
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
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    41
## run it!
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    42
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    43
MLTEXT="$EXIT $COMMIT $MLTEXT"
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    44
MLEXIT="commit();"
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    45
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    46
if [ -z "$TERMINATE" ]; then
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    47
  FEEDER_OPTS=""
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    48
else
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    49
  FEEDER_OPTS="-q"
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    50
fi
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    51
9789
wenzelm
parents: 9253
diff changeset
    52
"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
9794
2be239143d42 fixed quoting;
wenzelm
parents: 9789
diff changeset
    53
  { read FPID; "$ML_HOME"/$MOSML $ML_OPTIONS 2>&1; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
9789
wenzelm
parents: 9253
diff changeset
    54
RC="$?"
9253
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    55
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    56
[ -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
    57
9789
wenzelm
parents: 9253
diff changeset
    58
exit "$RC"