lib/scripts/run-smlnj
author webertj
Fri, 17 Aug 2012 20:31:12 +0200
changeset 48853 ec82c33c75f8
parent 48662 b171bcd5dd86
child 53657 64942a1f7187
permissions -rwxr-xr-x
Typo fixed.
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
2302
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
     2
#
9789
wenzelm
parents: 6078
diff changeset
     3
# Author: Markus Wenzel, TU Muenchen
2313
d97eef398257 replaced cat by ucat;
wenzelm
parents: 2302
diff changeset
     4
#
5708
fb09ab6a447f dropped support for SML/NJ 109.x;
wenzelm
parents: 5063
diff changeset
     5
# SML/NJ startup script (for 110 or later).
9977
32955afeb835 unexport exports;
wenzelm
parents: 9789
diff changeset
     6
31317
1f5740424c69 removed "compress" option from isabelle-process and isabelle usedir -- this is always enabled;
wenzelm
parents: 31315
diff changeset
     7
export -n INFILE OUTFILE MLTEXT TERMINATE NOWRITE
2302
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
     8
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
     9
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    10
## diagnostics
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    11
40544
34e56a6668ba tuned error messages;
wenzelm
parents: 39619
diff changeset
    12
function fail()
34e56a6668ba tuned error messages;
wenzelm
parents: 39619
diff changeset
    13
{
34e56a6668ba tuned error messages;
wenzelm
parents: 39619
diff changeset
    14
  echo "$1" >&2
34e56a6668ba tuned error messages;
wenzelm
parents: 39619
diff changeset
    15
  exit 2
34e56a6668ba tuned error messages;
wenzelm
parents: 39619
diff changeset
    16
}
34e56a6668ba tuned error messages;
wenzelm
parents: 39619
diff changeset
    17
2349
e9475a7be4ad various fixes;
wenzelm
parents: 2316
diff changeset
    18
function fail_out()
2302
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    19
{
40544
34e56a6668ba tuned error messages;
wenzelm
parents: 39619
diff changeset
    20
  fail "Unable to create output heap file: \"$OUTFILE\""
2302
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    21
}
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    22
5063
d45ec8d00ab0 check_mlhome_file;
wenzelm
parents: 4505
diff changeset
    23
function check_mlhome_file()
d45ec8d00ab0 check_mlhome_file;
wenzelm
parents: 4505
diff changeset
    24
{
40544
34e56a6668ba tuned error messages;
wenzelm
parents: 39619
diff changeset
    25
  [ ! -f "$1" ] && fail "Unable to locate \"$1\""
5063
d45ec8d00ab0 check_mlhome_file;
wenzelm
parents: 4505
diff changeset
    26
}
d45ec8d00ab0 check_mlhome_file;
wenzelm
parents: 4505
diff changeset
    27
6078
e01e2328d0f0 more robust heap file detection;
wenzelm
parents: 5708
diff changeset
    28
function check_heap_file()
e01e2328d0f0 more robust heap file detection;
wenzelm
parents: 5708
diff changeset
    29
{
e01e2328d0f0 more robust heap file detection;
wenzelm
parents: 5708
diff changeset
    30
  if [ ! -f "$1" ]; then
e01e2328d0f0 more robust heap file detection;
wenzelm
parents: 5708
diff changeset
    31
    echo "Expected to find ML heap file $1" >&2
e01e2328d0f0 more robust heap file detection;
wenzelm
parents: 5708
diff changeset
    32
    return 1
e01e2328d0f0 more robust heap file detection;
wenzelm
parents: 5708
diff changeset
    33
  else
e01e2328d0f0 more robust heap file detection;
wenzelm
parents: 5708
diff changeset
    34
    return 0
e01e2328d0f0 more robust heap file detection;
wenzelm
parents: 5708
diff changeset
    35
  fi
e01e2328d0f0 more robust heap file detection;
wenzelm
parents: 5708
diff changeset
    36
}
e01e2328d0f0 more robust heap file detection;
wenzelm
parents: 5708
diff changeset
    37
e01e2328d0f0 more robust heap file detection;
wenzelm
parents: 5708
diff changeset
    38
5063
d45ec8d00ab0 check_mlhome_file;
wenzelm
parents: 4505
diff changeset
    39
d45ec8d00ab0 check_mlhome_file;
wenzelm
parents: 4505
diff changeset
    40
## compiler binaries
d45ec8d00ab0 check_mlhome_file;
wenzelm
parents: 4505
diff changeset
    41
40544
34e56a6668ba tuned error messages;
wenzelm
parents: 39619
diff changeset
    42
[ -z "$ML_HOME" ] && fail "Missing ML installation (ML_HOME)"
34e56a6668ba tuned error messages;
wenzelm
parents: 39619
diff changeset
    43
5063
d45ec8d00ab0 check_mlhome_file;
wenzelm
parents: 4505
diff changeset
    44
SML="$ML_HOME/sml"
d45ec8d00ab0 check_mlhome_file;
wenzelm
parents: 4505
diff changeset
    45
ARCH_N_OPSYS="$ML_HOME/.arch-n-opsys"
d45ec8d00ab0 check_mlhome_file;
wenzelm
parents: 4505
diff changeset
    46
d45ec8d00ab0 check_mlhome_file;
wenzelm
parents: 4505
diff changeset
    47
check_mlhome_file "$SML"
d45ec8d00ab0 check_mlhome_file;
wenzelm
parents: 4505
diff changeset
    48
check_mlhome_file "$ARCH_N_OPSYS"
d45ec8d00ab0 check_mlhome_file;
wenzelm
parents: 4505
diff changeset
    49
d45ec8d00ab0 check_mlhome_file;
wenzelm
parents: 4505
diff changeset
    50
2302
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    51
3046
6b7935317538 adapted to SML/NJ 1.09.27;
wenzelm
parents: 3010
diff changeset
    52
## prepare databases
6b7935317538 adapted to SML/NJ 1.09.27;
wenzelm
parents: 3010
diff changeset
    53
4505
4a2c872b6513 use feeder to pipe into ML;
wenzelm
parents: 4415
diff changeset
    54
if [ -z "$INFILE" ]; then
48662
b171bcd5dd86 more informative process exit code;
wenzelm
parents: 48002
diff changeset
    55
  EXIT="fun exit rc : unit = Posix.Process.exit (Word8.fromInt rc);"
4505
4a2c872b6513 use feeder to pipe into ML;
wenzelm
parents: 4415
diff changeset
    56
  DB=""
4a2c872b6513 use feeder to pipe into ML;
wenzelm
parents: 4415
diff changeset
    57
else
4a2c872b6513 use feeder to pipe into ML;
wenzelm
parents: 4415
diff changeset
    58
  EXIT=""
3046
6b7935317538 adapted to SML/NJ 1.09.27;
wenzelm
parents: 3010
diff changeset
    59
  DB="@SMLload=$INFILE"
2349
e9475a7be4ad various fixes;
wenzelm
parents: 2316
diff changeset
    60
fi
e9475a7be4ad various fixes;
wenzelm
parents: 2316
diff changeset
    61
4505
4a2c872b6513 use feeder to pipe into ML;
wenzelm
parents: 4415
diff changeset
    62
if [ -z "$OUTFILE" ]; then
39619
34952c2423c6 isabelle-process: less verbose no-commit mode;
wenzelm
parents: 31317
diff changeset
    63
  COMMIT='fun commit () = false;'
34952c2423c6 isabelle-process: less verbose no-commit mode;
wenzelm
parents: 31317
diff changeset
    64
  MLEXIT=""
4505
4a2c872b6513 use feeder to pipe into ML;
wenzelm
parents: 4415
diff changeset
    65
else
4a2c872b6513 use feeder to pipe into ML;
wenzelm
parents: 4415
diff changeset
    66
  COMMIT="fun commit () = not (SMLofNJ.exportML\"$OUTFILE\");"
4a2c872b6513 use feeder to pipe into ML;
wenzelm
parents: 4415
diff changeset
    67
  [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
39619
34952c2423c6 isabelle-process: less verbose no-commit mode;
wenzelm
parents: 31317
diff changeset
    68
  MLEXIT="commit();"
4505
4a2c872b6513 use feeder to pipe into ML;
wenzelm
parents: 4415
diff changeset
    69
fi
2302
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    70
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    71
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    72
## run it!
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    73
4505
4a2c872b6513 use feeder to pipe into ML;
wenzelm
parents: 4415
diff changeset
    74
MLTEXT="$EXIT $COMMIT $MLTEXT"
2302
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    75
4505
4a2c872b6513 use feeder to pipe into ML;
wenzelm
parents: 4415
diff changeset
    76
if [ -z "$TERMINATE" ]; then
4a2c872b6513 use feeder to pipe into ML;
wenzelm
parents: 4415
diff changeset
    77
  FEEDER_OPTS=""
2302
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    78
else
4505
4a2c872b6513 use feeder to pipe into ML;
wenzelm
parents: 4415
diff changeset
    79
  FEEDER_OPTS="-q"
2302
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    80
fi
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    81
9789
wenzelm
parents: 6078
diff changeset
    82
"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
48002
6de952f4069f potentially more convincing kill -TERM of feeder (cf. 32c03d45fffe) -- attempt to workaround spurious perl "hangs" on lxbroy10;
wenzelm
parents: 40544
diff changeset
    83
  { read FPID; "$SML" $ML_OPTIONS "$DB"; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }
9789
wenzelm
parents: 6078
diff changeset
    84
RC="$?"
4505
4a2c872b6513 use feeder to pipe into ML;
wenzelm
parents: 4415
diff changeset
    85
4a2c872b6513 use feeder to pipe into ML;
wenzelm
parents: 4415
diff changeset
    86
4a2c872b6513 use feeder to pipe into ML;
wenzelm
parents: 4415
diff changeset
    87
## fix heap file name and permissions
3046
6b7935317538 adapted to SML/NJ 1.09.27;
wenzelm
parents: 3010
diff changeset
    88
4505
4a2c872b6513 use feeder to pipe into ML;
wenzelm
parents: 4415
diff changeset
    89
if [ -n "$OUTFILE" ]; then
9789
wenzelm
parents: 6078
diff changeset
    90
  eval $("$ARCH_N_OPSYS")
6078
e01e2328d0f0 more robust heap file detection;
wenzelm
parents: 5708
diff changeset
    91
  [ -z "$HEAP_SUFFIX" ] && HEAP_SUFFIX="$ARCH-$OPSYS"
e01e2328d0f0 more robust heap file detection;
wenzelm
parents: 5708
diff changeset
    92
  HEAP="$OUTFILE.$HEAP_SUFFIX"
e01e2328d0f0 more robust heap file detection;
wenzelm
parents: 5708
diff changeset
    93
  check_heap_file "$HEAP" && mv "$HEAP" "$OUTFILE" && \
4505
4a2c872b6513 use feeder to pipe into ML;
wenzelm
parents: 4415
diff changeset
    94
    [ -n "$NOWRITE" ] && chmod -w "$OUTFILE"
4a2c872b6513 use feeder to pipe into ML;
wenzelm
parents: 4415
diff changeset
    95
fi
3503
390093b95cb0 NOWRITE;
wenzelm
parents: 3055
diff changeset
    96
9789
wenzelm
parents: 6078
diff changeset
    97
exit "$RC"