lib/scripts/run-smlnj
author nipkow
Wed Aug 26 19:54:19 2009 +0200 (2009-08-26)
changeset 32416 4ea7648b6ae2
parent 31317 1f5740424c69
child 39619 34952c2423c6
permissions -rwxr-xr-x
merged
wenzelm@10555
     1
#!/usr/bin/env bash
wenzelm@2302
     2
#
wenzelm@9789
     3
# Author: Markus Wenzel, TU Muenchen
wenzelm@2313
     4
#
wenzelm@5708
     5
# SML/NJ startup script (for 110 or later).
wenzelm@9977
     6
wenzelm@31317
     7
export -n INFILE OUTFILE MLTEXT TERMINATE NOWRITE
wenzelm@2302
     8
wenzelm@2302
     9
wenzelm@2302
    10
## diagnostics
wenzelm@2302
    11
wenzelm@2349
    12
function fail_out()
wenzelm@2302
    13
{
wenzelm@2349
    14
  echo "Unable to create output heap file: \"$OUTFILE\"" >&2
wenzelm@2302
    15
  exit 2
wenzelm@2302
    16
}
wenzelm@2302
    17
wenzelm@5063
    18
function check_mlhome_file()
wenzelm@5063
    19
{
wenzelm@5063
    20
  if [ ! -f "$1" ]; then
wenzelm@5063
    21
    echo "Unable to locate $1" >&2
wenzelm@5063
    22
    echo "Please check your ML_HOME setting!" >&2
wenzelm@5063
    23
    exit 2
wenzelm@5063
    24
  fi
wenzelm@5063
    25
}
wenzelm@5063
    26
wenzelm@6078
    27
function check_heap_file()
wenzelm@6078
    28
{
wenzelm@6078
    29
  if [ ! -f "$1" ]; then
wenzelm@6078
    30
    echo "Expected to find ML heap file $1" >&2
wenzelm@6078
    31
    return 1
wenzelm@6078
    32
  else
wenzelm@6078
    33
    return 0
wenzelm@6078
    34
  fi
wenzelm@6078
    35
}
wenzelm@6078
    36
wenzelm@6078
    37
wenzelm@5063
    38
wenzelm@5063
    39
## compiler binaries
wenzelm@5063
    40
wenzelm@5063
    41
SML="$ML_HOME/sml"
wenzelm@5063
    42
ARCH_N_OPSYS="$ML_HOME/.arch-n-opsys"
wenzelm@5063
    43
wenzelm@5063
    44
check_mlhome_file "$SML"
wenzelm@5063
    45
check_mlhome_file "$ARCH_N_OPSYS"
wenzelm@5063
    46
wenzelm@5063
    47
wenzelm@2302
    48
wenzelm@3046
    49
## prepare databases
wenzelm@3046
    50
wenzelm@4505
    51
if [ -z "$INFILE" ]; then
wenzelm@4505
    52
  EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;"
wenzelm@4505
    53
  DB=""
wenzelm@4505
    54
else
wenzelm@4505
    55
  EXIT=""
wenzelm@3046
    56
  DB="@SMLload=$INFILE"
wenzelm@2349
    57
fi
wenzelm@2349
    58
wenzelm@4505
    59
if [ -z "$OUTFILE" ]; then
wenzelm@4505
    60
  COMMIT='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\n"); false);'
wenzelm@4505
    61
else
wenzelm@4505
    62
  COMMIT="fun commit () = not (SMLofNJ.exportML\"$OUTFILE\");"
wenzelm@4505
    63
  [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
wenzelm@4505
    64
fi
wenzelm@2302
    65
wenzelm@2302
    66
wenzelm@2302
    67
## run it!
wenzelm@2302
    68
wenzelm@4505
    69
MLTEXT="$EXIT $COMMIT $MLTEXT"
wenzelm@4505
    70
MLEXIT="commit();"
wenzelm@2302
    71
wenzelm@4505
    72
if [ -z "$TERMINATE" ]; then
wenzelm@4505
    73
  FEEDER_OPTS=""
wenzelm@2302
    74
else
wenzelm@4505
    75
  FEEDER_OPTS="-q"
wenzelm@2302
    76
fi
wenzelm@2302
    77
wenzelm@9789
    78
"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
wenzelm@9789
    79
  { read FPID; "$SML" $ML_OPTIONS "$DB"; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
wenzelm@9789
    80
RC="$?"
wenzelm@4505
    81
wenzelm@4505
    82
wenzelm@4505
    83
## fix heap file name and permissions
wenzelm@3046
    84
wenzelm@4505
    85
if [ -n "$OUTFILE" ]; then
wenzelm@9789
    86
  eval $("$ARCH_N_OPSYS")
wenzelm@6078
    87
  [ -z "$HEAP_SUFFIX" ] && HEAP_SUFFIX="$ARCH-$OPSYS"
wenzelm@6078
    88
  HEAP="$OUTFILE.$HEAP_SUFFIX"
wenzelm@6078
    89
  check_heap_file "$HEAP" && mv "$HEAP" "$OUTFILE" && \
wenzelm@4505
    90
    [ -n "$NOWRITE" ] && chmod -w "$OUTFILE"
wenzelm@4505
    91
fi
wenzelm@3503
    92
wenzelm@9789
    93
exit "$RC"