lib/scripts/run-poplogml
author wenzelm
Tue, 21 Nov 2006 18:07:33 +0100
changeset 21437 a3c55b85cf0e
parent 17820 9822a7755ad4
permissions -rwxr-xr-x
moved theorem kinds from PureThy to Thm;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
17759
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
     1
#!/usr/bin/env bash
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
     2
#
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
     3
# $Id$
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
     4
# Author: Makarius
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
     5
#
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
     6
# Poplog/PML startup script (version 15.6/2.1).
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
     7
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
     8
export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
     9
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
    10
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
    11
## diagnostics
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
    12
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
    13
function fail_out()
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
    14
{
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
    15
  echo "Unable to create output heap file: \"$OUTFILE\"" >&2
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
    16
  exit 2
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
    17
}
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
    18
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
    19
function check_mlhome_file()
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
    20
{
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
    21
  if [ ! -f "$1" ]; then
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
    22
    echo "Unable to locate $1" >&2
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
    23
    echo "Please check your ML_HOME setting!" >&2
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
    24
    exit 2
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
    25
  fi
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
    26
}
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
    27
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
    28
function check_heap_file()
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
    29
{
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
    30
  if [ ! -f "$1" ]; then
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
    31
    echo "Expected to find ML heap file $1" >&2
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
    32
    return 1
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
    33
  else
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
    34
    return 0
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
    35
  fi
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
    36
}
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
    37
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
    38
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
    39
## prepare databases
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
    40
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
    41
if [ -z "$INFILE" ]; then
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
    42
  EXIT="fun exit (i: int) = OS.execve \"/bin/sh\" [\"sh\", \"-c\", \"exit \" ^ makestring i] (OS.envlist());"
17794
87fe1dd02d34 initial pop11 code for ML use/use_string;
wenzelm
parents: 17759
diff changeset
    43
  USE='pop11
87fe1dd02d34 initial pop11 code for ML use/use_string;
wenzelm
parents: 17759
diff changeset
    44
section $-ml;
87fe1dd02d34 initial pop11 code for ML use/use_string;
wenzelm
parents: 17759
diff changeset
    45
87fe1dd02d34 initial pop11 code for ML use/use_string;
wenzelm
parents: 17759
diff changeset
    46
ml_exception Use of string;
87fe1dd02d34 initial pop11 code for ML use/use_string;
wenzelm
parents: 17759
diff changeset
    47
87fe1dd02d34 initial pop11 code for ML use/use_string;
wenzelm
parents: 17759
diff changeset
    48
ml_val use : string -> unit =
87fe1dd02d34 initial pop11 code for ML use/use_string;
wenzelm
parents: 17759
diff changeset
    49
procedure(name) with_props use;
87fe1dd02d34 initial pop11 code for ML use/use_string;
wenzelm
parents: 17759
diff changeset
    50
        lvars name, path;
87fe1dd02d34 initial pop11 code for ML use/use_string;
wenzelm
parents: 17759
diff changeset
    51
        lconstant UseExn = exception("Use");
87fe1dd02d34 initial pop11 code for ML use/use_string;
wenzelm
parents: 17759
diff changeset
    52
87fe1dd02d34 initial pop11 code for ML use/use_string;
wenzelm
parents: 17759
diff changeset
    53
        define dlocal pop_exception_handler(n, msg, idstring, severity);
87fe1dd02d34 initial pop11 code for ML use/use_string;
wenzelm
parents: 17759
diff changeset
    54
                returnunless(severity == `E` or severity == `R`)(false);
87fe1dd02d34 initial pop11 code for ML use/use_string;
wenzelm
parents: 17759
diff changeset
    55
                erasenum(n);
87fe1dd02d34 initial pop11 code for ML use/use_string;
wenzelm
parents: 17759
diff changeset
    56
                raise(UseExn(name));
87fe1dd02d34 initial pop11 code for ML use/use_string;
wenzelm
parents: 17759
diff changeset
    57
        enddefine;
87fe1dd02d34 initial pop11 code for ML use/use_string;
wenzelm
parents: 17759
diff changeset
    58
87fe1dd02d34 initial pop11 code for ML use/use_string;
wenzelm
parents: 17759
diff changeset
    59
        unless sourcefile(name) ->> path then raise(UseExn(name)) endunless;
87fe1dd02d34 initial pop11 code for ML use/use_string;
wenzelm
parents: 17759
diff changeset
    60
        ml_load(path);
87fe1dd02d34 initial pop11 code for ML use/use_string;
wenzelm
parents: 17759
diff changeset
    61
        ml_unit;
87fe1dd02d34 initial pop11 code for ML use/use_string;
wenzelm
parents: 17759
diff changeset
    62
endprocedure;
87fe1dd02d34 initial pop11 code for ML use/use_string;
wenzelm
parents: 17759
diff changeset
    63
87fe1dd02d34 initial pop11 code for ML use/use_string;
wenzelm
parents: 17759
diff changeset
    64
ml_val use_string : string -> unit =
87fe1dd02d34 initial pop11 code for ML use/use_string;
wenzelm
parents: 17759
diff changeset
    65
procedure(str) with_props use_string;
87fe1dd02d34 initial pop11 code for ML use/use_string;
wenzelm
parents: 17759
diff changeset
    66
        lvars str;
87fe1dd02d34 initial pop11 code for ML use/use_string;
wenzelm
parents: 17759
diff changeset
    67
        lconstant UseExn = exception("Use");
87fe1dd02d34 initial pop11 code for ML use/use_string;
wenzelm
parents: 17759
diff changeset
    68
87fe1dd02d34 initial pop11 code for ML use/use_string;
wenzelm
parents: 17759
diff changeset
    69
        define dlocal pop_exception_handler(n, msg, idstring, severity);
17820
9822a7755ad4 cleanup backup images;
wenzelm
parents: 17807
diff changeset
    70
                [n ^n msg ^msg  idstring ^idstring severity ^severity] ==>
17794
87fe1dd02d34 initial pop11 code for ML use/use_string;
wenzelm
parents: 17759
diff changeset
    71
                returnunless(severity == `E` or severity == `R`)(false);
87fe1dd02d34 initial pop11 code for ML use/use_string;
wenzelm
parents: 17759
diff changeset
    72
                erasenum(n);
87fe1dd02d34 initial pop11 code for ML use/use_string;
wenzelm
parents: 17759
diff changeset
    73
                raise(UseExn(str));
87fe1dd02d34 initial pop11 code for ML use/use_string;
wenzelm
parents: 17759
diff changeset
    74
        enddefine;
87fe1dd02d34 initial pop11 code for ML use/use_string;
wenzelm
parents: 17759
diff changeset
    75
87fe1dd02d34 initial pop11 code for ML use/use_string;
wenzelm
parents: 17759
diff changeset
    76
        ml_compile(stringin(str));
87fe1dd02d34 initial pop11 code for ML use/use_string;
wenzelm
parents: 17759
diff changeset
    77
        ml_unit;
87fe1dd02d34 initial pop11 code for ML use/use_string;
wenzelm
parents: 17759
diff changeset
    78
endprocedure;
87fe1dd02d34 initial pop11 code for ML use/use_string;
wenzelm
parents: 17759
diff changeset
    79
87fe1dd02d34 initial pop11 code for ML use/use_string;
wenzelm
parents: 17759
diff changeset
    80
endsection;
87fe1dd02d34 initial pop11 code for ML use/use_string;
wenzelm
parents: 17759
diff changeset
    81
ml'
17759
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
    82
  DB=""
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
    83
else
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
    84
  EXIT=""
17794
87fe1dd02d34 initial pop11 code for ML use/use_string;
wenzelm
parents: 17759
diff changeset
    85
  USE=""
17759
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
    86
  DB="+$INFILE"
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
    87
fi
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
    88
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
    89
if [ -z "$OUTFILE" ]; then
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
    90
  COMMIT='fun commit () = (StdIO.output (StdIO.std_err, "Error - Database is not opened for writing.\n"); false);'
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
    91
else
17805
a9c2d42937dd -nort option;
wenzelm
parents: 17794
diff changeset
    92
  ML_OPTIONS="$ML_OPTIONS -nort"
17759
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
    93
  if [ -z "$NOWRITE" ]; then
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
    94
    COMMIT="fun commit () = if System.make {image =\"$OUTFILE\", lock = false, share = false, banner = false, init = false} then System.restart() else true;"
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
    95
  else
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
    96
    COMMIT="fun commit () = if System.make {image =\"$OUTFILE\", lock = true, share = true, banner = false, init = false} then System.restart() else true;"
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
    97
  fi
17794
87fe1dd02d34 initial pop11 code for ML use/use_string;
wenzelm
parents: 17759
diff changeset
    98
  [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
17759
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
    99
fi
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
   100
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
   101
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
   102
## run it!
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
   103
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
   104
POPLOG="$ML_HOME/poplog"
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
   105
check_mlhome_file "$POPLOG"
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
   106
17807
cc5dbc24e561 get rid of feeder -- at the cost of batch-only commit-at-exit;
wenzelm
parents: 17805
diff changeset
   107
INIT="$ISABELLE_TMP/init.ml"
cc5dbc24e561 get rid of feeder -- at the cost of batch-only commit-at-exit;
wenzelm
parents: 17805
diff changeset
   108
echo 'pop11
cc5dbc24e561 get rid of feeder -- at the cost of batch-only commit-at-exit;
wenzelm
parents: 17805
diff changeset
   109
section $-ml;
cc5dbc24e561 get rid of feeder -- at the cost of batch-only commit-at-exit;
wenzelm
parents: 17805
diff changeset
   110
false -> ml_quiet;
cc5dbc24e561 get rid of feeder -- at the cost of batch-only commit-at-exit;
wenzelm
parents: 17805
diff changeset
   111
endsection;
cc5dbc24e561 get rid of feeder -- at the cost of batch-only commit-at-exit;
wenzelm
parents: 17805
diff changeset
   112
ml' > "$INIT"
17759
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
   113
17807
cc5dbc24e561 get rid of feeder -- at the cost of batch-only commit-at-exit;
wenzelm
parents: 17805
diff changeset
   114
echo "$EXIT $USE $COMMIT $MLTEXT" >> "$INIT"
cc5dbc24e561 get rid of feeder -- at the cost of batch-only commit-at-exit;
wenzelm
parents: 17805
diff changeset
   115
cc5dbc24e561 get rid of feeder -- at the cost of batch-only commit-at-exit;
wenzelm
parents: 17805
diff changeset
   116
if [ -n "$TERMINATE" ]; then
cc5dbc24e561 get rid of feeder -- at the cost of batch-only commit-at-exit;
wenzelm
parents: 17805
diff changeset
   117
  ML_OPTIONS="$ML_OPTIONS -nostdin"
cc5dbc24e561 get rid of feeder -- at the cost of batch-only commit-at-exit;
wenzelm
parents: 17805
diff changeset
   118
  echo "commit();" >> "$INIT"
17759
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
   119
fi
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
   120
17807
cc5dbc24e561 get rid of feeder -- at the cost of batch-only commit-at-exit;
wenzelm
parents: 17805
diff changeset
   121
"$POPLOG" pml "$DB" $ML_OPTIONS -load "$INIT" 2>&1
17759
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
   122
RC="$?"
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
   123
17807
cc5dbc24e561 get rid of feeder -- at the cost of batch-only commit-at-exit;
wenzelm
parents: 17805
diff changeset
   124
rm -f "$INIT"
17759
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
   125
17820
9822a7755ad4 cleanup backup images;
wenzelm
parents: 17807
diff changeset
   126
if [ -n "$OUTFILE" ] && check_heap_file "$OUTFILE"; then
17794
87fe1dd02d34 initial pop11 code for ML use/use_string;
wenzelm
parents: 17759
diff changeset
   127
  [ -n "$NOWRITE" ] && chmod -w "$OUTFILE"
17820
9822a7755ad4 cleanup backup images;
wenzelm
parents: 17807
diff changeset
   128
  rm -f "$OUTFILE-"
9822a7755ad4 cleanup backup images;
wenzelm
parents: 17807
diff changeset
   129
fi
17759
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
   130
dce4b7eb69c0 Poplog/PML startup script.
wenzelm
parents:
diff changeset
   131
exit "$RC"