lib/scripts/run-polyml-5.5.2
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@52832
     1
#!/usr/bin/env bash
wenzelm@52832
     2
# :mode=shellscript:
wenzelm@52832
     3
#
wenzelm@52832
     4
# Author: Makarius
wenzelm@52832
     5
#
wenzelm@54717
     6
# Startup script for Poly/ML 5.5.2.
wenzelm@52832
     7
wenzelm@52832
     8
export -n INFILE OUTFILE MLTEXT TERMINATE NOWRITE
wenzelm@52832
     9
wenzelm@52832
    10
wenzelm@52832
    11
## diagnostics
wenzelm@52832
    12
wenzelm@52832
    13
function fail()
wenzelm@52832
    14
{
wenzelm@52832
    15
  echo "$1" >&2
wenzelm@52832
    16
  exit 2
wenzelm@52832
    17
}
wenzelm@52832
    18
wenzelm@52832
    19
function fail_out()
wenzelm@52832
    20
{
wenzelm@52832
    21
  fail "Unable to create output heap file: \"$OUTFILE\""
wenzelm@52832
    22
}
wenzelm@52832
    23
wenzelm@52832
    24
function check_file()
wenzelm@52832
    25
{
wenzelm@52832
    26
  [ ! -f "$1" ] && fail "Unable to locate \"$1\""
wenzelm@52832
    27
}
wenzelm@52832
    28
wenzelm@52832
    29
wenzelm@52832
    30
## compiler executables and libraries
wenzelm@52832
    31
wenzelm@52832
    32
[ -z "$ML_HOME" ] && fail "Missing ML installation (ML_HOME)"
wenzelm@52832
    33
wenzelm@52832
    34
POLY="$ML_HOME/poly"
wenzelm@52832
    35
check_file "$POLY"
wenzelm@52832
    36
wenzelm@52832
    37
librarypath "$ML_HOME"
wenzelm@52832
    38
wenzelm@52832
    39
wenzelm@52832
    40
wenzelm@52832
    41
## prepare databases
wenzelm@52832
    42
wenzelm@52832
    43
if [ -z "$INFILE" ]; then
wenzelm@52832
    44
  INIT=""
wenzelm@56627
    45
  EXIT="fun exit rc = Posix.Process.exit (Word8.fromInt rc);"
wenzelm@52832
    46
else
wenzelm@52832
    47
  check_file "$INFILE"
wenzelm@52832
    48
  INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())); PolyML.SaveState.loadState \"$INFILE\" handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $INFILE\\n\"); Posix.Process.exit 0w1));"
wenzelm@52832
    49
  EXIT=""
wenzelm@52832
    50
fi
wenzelm@52832
    51
wenzelm@52832
    52
if [ -z "$OUTFILE" ]; then
wenzelm@52832
    53
  COMMIT='fun commit () = false;'
wenzelm@52832
    54
  MLEXIT=""
wenzelm@52832
    55
else
wenzelm@53657
    56
  if [ -z "$INFILE" ]; then
wenzelm@53657
    57
    COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$OUTFILE\"; true) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $OUTFILE\\n\"); Posix.Process.exit 0w1);"
wenzelm@53657
    58
  else
wenzelm@53657
    59
    COMMIT="fun commit () = (ML_System.share_common_data (); ML_System.save_state \"$OUTFILE\");"
wenzelm@53657
    60
  fi
wenzelm@52832
    61
  [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
wenzelm@52832
    62
  MLEXIT="commit();"
wenzelm@52832
    63
fi
wenzelm@52832
    64
wenzelm@52832
    65
wenzelm@52832
    66
## run it!
wenzelm@52832
    67
wenzelm@52832
    68
MLTEXT="$INIT $EXIT $COMMIT $MLTEXT"
wenzelm@52832
    69
wenzelm@52832
    70
if [ -n "$TERMINATE" -a -z "$MLEXIT" ]; then
wenzelm@52835
    71
  "$POLY" -q -i $ML_OPTIONS --eval "$(perl "$ISABELLE_HOME/lib/scripts/recode.pl" "$MLTEXT")" \
wenzelm@52835
    72
    --error-exit </dev/null
wenzelm@52832
    73
  RC="$?"
wenzelm@52832
    74
else
wenzelm@52832
    75
  if [ -z "$TERMINATE" ]; then
wenzelm@52832
    76
    FEEDER_OPTS=""
wenzelm@52832
    77
  else
wenzelm@52832
    78
    FEEDER_OPTS="-q"
wenzelm@52833
    79
    ML_OPTIONS="$ML_OPTIONS --error-exit"
wenzelm@52832
    80
  fi
wenzelm@52832
    81
  "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
wenzelm@52832
    82
    { read FPID; "$POLY" -q -i $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }
wenzelm@52832
    83
  RC="$?"
wenzelm@52832
    84
fi
wenzelm@52832
    85
wenzelm@52832
    86
[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
wenzelm@52832
    87
wenzelm@52832
    88
exit "$RC"
wenzelm@52832
    89
wenzelm@52832
    90
#:wrap=soft:maxLineLen=100: