lib/scripts/run-smlnj-0.93
author wenzelm
Sat, 24 Nov 2001 16:54:32 +0100
changeset 12282 f98beaaa7c4f
parent 10555 2323ec838401
permissions -rwxr-xr-x
generic_merge;
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
2411
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
     2
#
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
     3
# $Id$
9789
wenzelm
parents: 5063
diff changeset
     4
# Author: Markus Wenzel, TU Muenchen
wenzelm
parents: 5063
diff changeset
     5
# License: GPL (GNU GENERAL PUBLIC LICENSE)
2411
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
     6
#
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
     7
# SML/NJ startup script (for 0.93).
9977
32955afeb835 unexport exports;
wenzelm
parents: 9789
diff changeset
     8
10105
f9be78009930 added COPYDB argument;
wenzelm
parents: 9997
diff changeset
     9
export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE
2411
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    10
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    11
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    12
## diagnostics
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    13
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    14
function fail_out()
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    15
{
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    16
  echo "Unable to create output heap file: \"$OUTFILE\"" >&2
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    17
  exit 2
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    18
}
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    19
5063
d45ec8d00ab0 check_mlhome_file;
wenzelm
parents: 4513
diff changeset
    20
function check_mlhome_file()
d45ec8d00ab0 check_mlhome_file;
wenzelm
parents: 4513
diff changeset
    21
{
d45ec8d00ab0 check_mlhome_file;
wenzelm
parents: 4513
diff changeset
    22
  if [ ! -f "$1" ]; then
d45ec8d00ab0 check_mlhome_file;
wenzelm
parents: 4513
diff changeset
    23
    echo "Unable to locate $1" >&2
d45ec8d00ab0 check_mlhome_file;
wenzelm
parents: 4513
diff changeset
    24
    echo "Please check your ML_HOME setting!" >&2
d45ec8d00ab0 check_mlhome_file;
wenzelm
parents: 4513
diff changeset
    25
    exit 2
d45ec8d00ab0 check_mlhome_file;
wenzelm
parents: 4513
diff changeset
    26
  fi
d45ec8d00ab0 check_mlhome_file;
wenzelm
parents: 4513
diff changeset
    27
}
d45ec8d00ab0 check_mlhome_file;
wenzelm
parents: 4513
diff changeset
    28
2411
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    29
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    30
## prepare databases
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    31
2440
b3ac45aba238 fixed EXIT def;
wenzelm
parents: 2411
diff changeset
    32
if [ -z "$INFILE" ]; then
b3ac45aba238 fixed EXIT def;
wenzelm
parents: 2411
diff changeset
    33
  INFILE="$ML_HOME/sml"
5063
d45ec8d00ab0 check_mlhome_file;
wenzelm
parents: 4513
diff changeset
    34
  check_mlhome_file "$INFILE"
4513
6de428eac512 feeder;
wenzelm
parents: 4333
diff changeset
    35
  EXIT="val exit: int -> unit = System.Unsafe.CInterface.exit;"
2440
b3ac45aba238 fixed EXIT def;
wenzelm
parents: 2411
diff changeset
    36
else
b3ac45aba238 fixed EXIT def;
wenzelm
parents: 2411
diff changeset
    37
  EXIT=""
b3ac45aba238 fixed EXIT def;
wenzelm
parents: 2411
diff changeset
    38
fi
2411
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    39
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    40
MOVE=""
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    41
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    42
if [ -z "$OUTFILE" ]; then
4513
6de428eac512 feeder;
wenzelm
parents: 4333
diff changeset
    43
  COMMIT='fun commit () = (output (std_err, "Error - Database is not opened for writing.\n"); false);'
2411
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    44
else
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    45
  if [ "$INFILE" -ef "$OUTFILE" ]; then
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    46
    OUTDIR=$(dirname "$OUTFILE")/tmp
9789
wenzelm
parents: 5063
diff changeset
    47
    OUTFILE="$OUTDIR"/$(basename "$OUTFILE")
2411
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    48
    mkdir -p "$OUTDIR" || fail_out
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    49
    MOVE=true
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    50
  fi
2936
bd33e7aae062 fixed { ... } shell syntax to accomodate bash 2.x;
wenzelm
parents: 2622
diff changeset
    51
  [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
2411
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    52
  COMMIT="fun commit () = not (exportML\"$OUTFILE\");"
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    53
fi
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    54
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    55
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    56
## run it!
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    57
4513
6de428eac512 feeder;
wenzelm
parents: 4333
diff changeset
    58
MLTEXT="$EXIT $COMMIT $MLTEXT"
6de428eac512 feeder;
wenzelm
parents: 4333
diff changeset
    59
MLEXIT="commit();"
2411
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    60
4513
6de428eac512 feeder;
wenzelm
parents: 4333
diff changeset
    61
if [ -z "$TERMINATE" ]; then
6de428eac512 feeder;
wenzelm
parents: 4333
diff changeset
    62
  FEEDER_OPTS=""
2411
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    63
else
4513
6de428eac512 feeder;
wenzelm
parents: 4333
diff changeset
    64
  FEEDER_OPTS="-q"
2411
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    65
fi
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    66
9789
wenzelm
parents: 5063
diff changeset
    67
"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
wenzelm
parents: 5063
diff changeset
    68
  { read FPID; "$INFILE" $ML_OPTIONS; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
wenzelm
parents: 5063
diff changeset
    69
RC="$?"
4513
6de428eac512 feeder;
wenzelm
parents: 4333
diff changeset
    70
6de428eac512 feeder;
wenzelm
parents: 4333
diff changeset
    71
6de428eac512 feeder;
wenzelm
parents: 4333
diff changeset
    72
## fix heap file
6de428eac512 feeder;
wenzelm
parents: 4333
diff changeset
    73
6de428eac512 feeder;
wenzelm
parents: 4333
diff changeset
    74
[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
3503
390093b95cb0 NOWRITE;
wenzelm
parents: 3055
diff changeset
    75
2411
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    76
if [ -n "$MOVE" -a -f "$OUTFILE" ]; then
2551
fe15e3fcccf0 'rm -f' instead of 'mv -f';
wenzelm
parents: 2440
diff changeset
    77
  rm -f "$INFILE" || fail_out
fe15e3fcccf0 'rm -f' instead of 'mv -f';
wenzelm
parents: 2440
diff changeset
    78
  mv "$OUTFILE" "$INFILE" || fail_out
2411
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    79
fi
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    80
9789
wenzelm
parents: 5063
diff changeset
    81
exit "$RC"