2343
|
1 |
#!/bin/bash -norc
|
2292
|
2 |
#
|
2308
|
3 |
# $Id$
|
|
4 |
#
|
2292
|
5 |
# Basic Isabelle startup script.
|
|
6 |
|
|
7 |
|
|
8 |
## settings
|
|
9 |
|
2704
|
10 |
PRG=$(basename $0)
|
|
11 |
|
2292
|
12 |
ISABELLE_HOME=$(dirname $(dirname $0))
|
2704
|
13 |
case "$ISABELLE_HOME" in
|
|
14 |
/*)
|
|
15 |
if [ -f $ISABELLE_HOME/lib/scripts/getsettings ]; then
|
|
16 |
. $ISABELLE_HOME/lib/scripts/getsettings || exit 2
|
|
17 |
else
|
|
18 |
echo "ERROR: $PRG probably not called from its original place!"
|
|
19 |
exit 1
|
|
20 |
fi
|
|
21 |
;;
|
|
22 |
*)
|
|
23 |
echo "ERROR: $PRG not called with absolute path specification!"
|
|
24 |
exit 1
|
|
25 |
;;
|
|
26 |
esac
|
2292
|
27 |
|
|
28 |
|
|
29 |
## diagnostics
|
|
30 |
|
|
31 |
function usage()
|
|
32 |
{
|
|
33 |
echo
|
|
34 |
echo "Usage: $PRG [OPTIONS] [INPUT] [OUTPUT]"
|
|
35 |
echo
|
|
36 |
echo " Options are:"
|
2395
|
37 |
echo " -c force copying of heap file (for Poly/ML)"
|
2343
|
38 |
echo " -e MLTEXT pass MLTEXT to the ML session"
|
2704
|
39 |
echo " -m MODE add print mode for output"
|
2292
|
40 |
echo " -q non-interactive session"
|
|
41 |
echo " -r open heap file read-only"
|
2343
|
42 |
echo " -u pass 'exit_use_dir\".\";' to the ML session"
|
2292
|
43 |
echo
|
|
44 |
echo " INPUT (default \"$DEFAULT_LOGIC\") and OUTPUT specify in/out heaps."
|
|
45 |
echo " These are either names to be searched in the Isabelle path, or actual"
|
2343
|
46 |
echo " file names (then containing at least one /)."
|
2292
|
47 |
echo " If INPUT is \"SYSTEM\", just start the bare bones ML system."
|
|
48 |
echo
|
|
49 |
exit 1
|
|
50 |
}
|
|
51 |
|
|
52 |
function fail()
|
|
53 |
{
|
2343
|
54 |
echo "$1" >&2
|
2292
|
55 |
exit 2
|
|
56 |
}
|
|
57 |
|
|
58 |
|
|
59 |
## process command line
|
|
60 |
|
|
61 |
# options
|
|
62 |
|
|
63 |
COPYDB=""
|
|
64 |
MLTEXT=""
|
|
65 |
COPYDB=""
|
2704
|
66 |
MODES=""
|
2292
|
67 |
TERMINATE=""
|
|
68 |
READONLY=""
|
|
69 |
|
2704
|
70 |
while getopts "ce:m:qru" OPT
|
2292
|
71 |
do
|
|
72 |
case "$OPT" in
|
|
73 |
c)
|
|
74 |
COPYDB=true
|
|
75 |
;;
|
|
76 |
e)
|
|
77 |
MLTEXT="$MLTEXT $OPTARG"
|
|
78 |
;;
|
2704
|
79 |
m)
|
|
80 |
if [ -z "$MODES" ]; then
|
|
81 |
MODES="\"$OPTARG\""
|
|
82 |
else
|
2711
|
83 |
MODES="\"$OPTARG\", $MODES"
|
2704
|
84 |
fi
|
|
85 |
;;
|
2292
|
86 |
q)
|
|
87 |
TERMINATE=true
|
|
88 |
;;
|
|
89 |
r)
|
|
90 |
READONLY=true
|
|
91 |
;;
|
|
92 |
u)
|
2343
|
93 |
MLTEXT="$MLTEXT exit_use_dir\".\";"
|
2292
|
94 |
;;
|
|
95 |
\?)
|
|
96 |
usage
|
|
97 |
;;
|
|
98 |
esac
|
|
99 |
done
|
|
100 |
|
|
101 |
shift $(($OPTIND - 1))
|
|
102 |
|
|
103 |
|
|
104 |
# args
|
|
105 |
|
|
106 |
INPUT=""
|
|
107 |
OUTPUT=""
|
|
108 |
|
|
109 |
if [ $# -ge 1 ]; then
|
|
110 |
INPUT="$1"
|
|
111 |
shift
|
|
112 |
fi
|
|
113 |
|
|
114 |
if [ $# -ge 1 ]; then
|
|
115 |
OUTPUT="$1"
|
|
116 |
shift
|
|
117 |
fi
|
|
118 |
|
2343
|
119 |
[ $# -ne 0 ] && { echo "Bad args: $*"; usage }
|
2292
|
120 |
|
|
121 |
|
|
122 |
## check ML system
|
|
123 |
|
2308
|
124 |
[ -z "$ML_SYSTEM" ] && fail "Missing ML system settings! Unable to run Isabelle."
|
2292
|
125 |
|
|
126 |
|
|
127 |
## input heap file
|
|
128 |
|
|
129 |
[ -z "$INPUT" ] && INPUT="$DEFAULT_LOGIC"
|
|
130 |
|
|
131 |
case "$INPUT" in
|
|
132 |
SYSTEM)
|
|
133 |
INFILE=""
|
|
134 |
;;
|
|
135 |
*/*)
|
|
136 |
INFILE="$INPUT"
|
2343
|
137 |
[ ! -f "$INFILE" ] && fail "Bad heap file: \"$INFILE\""
|
2292
|
138 |
;;
|
|
139 |
*)
|
2308
|
140 |
ISA_PATH=""
|
2292
|
141 |
INFILE=""
|
|
142 |
for DIR in $(echo $ISABELLE_PATH | tr : " ")
|
|
143 |
do
|
2308
|
144 |
ISA_PATH="$ISA_PATH $DIR/$ML_SYSTEM-$PLATFORM"
|
2292
|
145 |
[ -z "$INFILE" -a -f $DIR/$ML_SYSTEM-$PLATFORM/$INPUT ] && INFILE=$DIR/$ML_SYSTEM-$PLATFORM/$INPUT
|
|
146 |
done
|
2308
|
147 |
if [ -z "$INFILE" ]; then
|
2343
|
148 |
echo "Unknown logic \"$INPUT\" -- no heap file found in:" >&2
|
2308
|
149 |
for DIR in $ISA_PATH
|
|
150 |
do
|
2343
|
151 |
echo " $DIR" >&2
|
2308
|
152 |
done
|
|
153 |
exit 2
|
|
154 |
fi
|
2292
|
155 |
;;
|
|
156 |
esac
|
|
157 |
|
|
158 |
|
|
159 |
## output heap file
|
|
160 |
|
|
161 |
case "$OUTPUT" in
|
|
162 |
"")
|
|
163 |
[ -z "$READONLY" -a -w "$INFILE" ] && OUTFILE="$INFILE"
|
|
164 |
;;
|
|
165 |
*/*)
|
|
166 |
OUTFILE="$OUTPUT"
|
|
167 |
;;
|
|
168 |
*)
|
|
169 |
OUTDIR="$ISABELLE_OUTPUT/$ML_SYSTEM-$PLATFORM"
|
|
170 |
mkdir -p "$OUTDIR"
|
|
171 |
OUTFILE="$OUTDIR/$OUTPUT"
|
|
172 |
;;
|
|
173 |
esac
|
|
174 |
|
|
175 |
|
|
176 |
## run it!
|
|
177 |
|
|
178 |
ML_SYSTEM_BASE=$(echo $ML_SYSTEM | cut -f1 -d-)
|
|
179 |
|
2704
|
180 |
[ -n "$MODES" ] && MLTEXT="print_mode := [$MODES]; $MLTEXT"
|
|
181 |
|
2343
|
182 |
export INFILE OUTFILE COPYDB MLTEXT TERMINATE
|
2292
|
183 |
[ -f $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM ] && exec $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM
|
|
184 |
exec $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE
|