lib/scripts/run-smlnj
author nipkow
Fri May 30 18:13:40 2014 +0200 (2014-05-30)
changeset 57136 653e56c6c963
parent 56627 cb912b7de3cf
child 59344 e0ce214303c1
permissions -rwxr-xr-x
must not cancel common factors on both sides of (in)equations in linear arithmetic decicision procedure
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@40544
    12
function fail()
wenzelm@40544
    13
{
wenzelm@40544
    14
  echo "$1" >&2
wenzelm@40544
    15
  exit 2
wenzelm@40544
    16
}
wenzelm@40544
    17
wenzelm@2349
    18
function fail_out()
wenzelm@2302
    19
{
wenzelm@40544
    20
  fail "Unable to create output heap file: \"$OUTFILE\""
wenzelm@2302
    21
}
wenzelm@2302
    22
wenzelm@5063
    23
function check_mlhome_file()
wenzelm@5063
    24
{
wenzelm@40544
    25
  [ ! -f "$1" ] && fail "Unable to locate \"$1\""
wenzelm@5063
    26
}
wenzelm@5063
    27
wenzelm@6078
    28
function check_heap_file()
wenzelm@6078
    29
{
wenzelm@6078
    30
  if [ ! -f "$1" ]; then
wenzelm@6078
    31
    echo "Expected to find ML heap file $1" >&2
wenzelm@6078
    32
    return 1
wenzelm@6078
    33
  else
wenzelm@6078
    34
    return 0
wenzelm@6078
    35
  fi
wenzelm@6078
    36
}
wenzelm@6078
    37
wenzelm@6078
    38
wenzelm@5063
    39
wenzelm@5063
    40
## compiler binaries
wenzelm@5063
    41
wenzelm@40544
    42
[ -z "$ML_HOME" ] && fail "Missing ML installation (ML_HOME)"
wenzelm@40544
    43
wenzelm@5063
    44
SML="$ML_HOME/sml"
wenzelm@5063
    45
ARCH_N_OPSYS="$ML_HOME/.arch-n-opsys"
wenzelm@5063
    46
wenzelm@5063
    47
check_mlhome_file "$SML"
wenzelm@5063
    48
check_mlhome_file "$ARCH_N_OPSYS"
wenzelm@5063
    49
wenzelm@53657
    50
eval $("$ARCH_N_OPSYS")
wenzelm@53657
    51
wenzelm@5063
    52
wenzelm@2302
    53
wenzelm@3046
    54
## prepare databases
wenzelm@3046
    55
wenzelm@4505
    56
if [ -z "$INFILE" ]; then
wenzelm@56627
    57
  EXIT="fun exit rc = Posix.Process.exit (Word8.fromInt rc);"
wenzelm@4505
    58
  DB=""
wenzelm@4505
    59
else
wenzelm@4505
    60
  EXIT=""
wenzelm@3046
    61
  DB="@SMLload=$INFILE"
wenzelm@2349
    62
fi
wenzelm@2349
    63
wenzelm@4505
    64
if [ -z "$OUTFILE" ]; then
wenzelm@39619
    65
  COMMIT='fun commit () = false;'
wenzelm@39619
    66
  MLEXIT=""
wenzelm@4505
    67
else
wenzelm@53657
    68
  if [ -z "$INFILE" ]; then
wenzelm@53657
    69
    COMMIT="fun commit () = if SMLofNJ.exportML \"$OUTFILE\" then () else OS.FileSys.rename {old = \"$OUTFILE.$ARCH-$OPSYS\", new = \"$OUTFILE\"};"
wenzelm@53657
    70
  else
wenzelm@53657
    71
    COMMIT="fun commit () = (ML_System.share_common_data (); ML_System.save_state \"$OUTFILE\");"
wenzelm@53657
    72
  fi
wenzelm@4505
    73
  [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
wenzelm@39619
    74
  MLEXIT="commit();"
wenzelm@4505
    75
fi
wenzelm@2302
    76
wenzelm@2302
    77
wenzelm@2302
    78
## run it!
wenzelm@2302
    79
wenzelm@4505
    80
MLTEXT="$EXIT $COMMIT $MLTEXT"
wenzelm@2302
    81
wenzelm@4505
    82
if [ -z "$TERMINATE" ]; then
wenzelm@4505
    83
  FEEDER_OPTS=""
wenzelm@2302
    84
else
wenzelm@4505
    85
  FEEDER_OPTS="-q"
wenzelm@2302
    86
fi
wenzelm@2302
    87
wenzelm@9789
    88
"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
wenzelm@48002
    89
  { read FPID; "$SML" $ML_OPTIONS "$DB"; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }
wenzelm@9789
    90
RC="$?"
wenzelm@4505
    91
wenzelm@4505
    92
wenzelm@4505
    93
## fix heap file name and permissions
wenzelm@3046
    94
wenzelm@4505
    95
if [ -n "$OUTFILE" ]; then
wenzelm@53657
    96
  check_heap_file "$OUTFILE" && [ -n "$NOWRITE" ] && chmod -w "$OUTFILE"
wenzelm@4505
    97
fi
wenzelm@3503
    98
wenzelm@9789
    99
exit "$RC"