2 # |
2 # |
3 # $Id$ |
3 # $Id$ |
4 # Author: Markus Wenzel, TU Muenchen |
4 # Author: Markus Wenzel, TU Muenchen |
5 # License: GPL (GNU GENERAL PUBLIC LICENSE) |
5 # License: GPL (GNU GENERAL PUBLIC LICENSE) |
6 # |
6 # |
7 # Basic Isabelle startup script. |
7 # Smart selection of isabelle-process versus isabelle-interface. |
8 |
8 |
|
9 THIS=$(cd "$(dirname "$0")"; pwd) |
|
10 NAME="$(basename "$0")" |
9 |
11 |
10 ## settings |
12 PRG=isabelle-interface |
|
13 [ "$NAME" = isabelle ] && PRG=isabelle-process |
11 |
14 |
12 PRG="$(basename "$0")" |
15 exec "$THIS/$PRG" "$@" |
13 |
|
14 ISABELLE_HOME="$(dirname "$0")/.." |
|
15 . "$ISABELLE_HOME/lib/scripts/getsettings" || \ |
|
16 { echo "$PRG probably not called from its original place!"; exit 2; } |
|
17 |
|
18 |
|
19 ## diagnostics |
|
20 |
|
21 function usage() |
|
22 { |
|
23 echo |
|
24 echo "Usage: $PRG [OPTIONS] [INPUT] [OUTPUT]" |
|
25 echo |
|
26 echo " Options are:" |
|
27 echo " -C tell ML system to copy output image" |
|
28 echo " -I startup Isar interaction mode" |
|
29 echo " -P startup Proof General interaction mode" |
|
30 echo " -c tell ML system to compress output image" |
|
31 echo " -e MLTEXT pass MLTEXT to the ML session" |
|
32 echo " -f pass 'Session.finish();' to the ML session" |
|
33 echo " -m MODE add print mode for output" |
|
34 echo " -q non-interactive session" |
|
35 echo " -r open heap file read-only" |
|
36 echo " -u pass 'use\"ROOT.ML\";' to the ML session" |
|
37 echo " -w reset write permissions on OUTPUT" |
|
38 echo |
|
39 echo " INPUT (default \"$ISABELLE_LOGIC\") and OUTPUT specify in/out heaps." |
|
40 echo " These are either names to be searched in the Isabelle path, or" |
|
41 echo " actual file names (containing at least one /)." |
|
42 echo " If INPUT is \"RAW_ML_SYSTEM\", just start the bare bones ML system." |
|
43 echo |
|
44 exit 1 |
|
45 } |
|
46 |
|
47 function fail() |
|
48 { |
|
49 echo "$1" >&2 |
|
50 exit 2 |
|
51 } |
|
52 |
|
53 |
|
54 ## process command line |
|
55 |
|
56 # options |
|
57 |
|
58 COPYDB="" |
|
59 ISAR=false |
|
60 PROOFGENERAL="" |
|
61 COMPRESS="" |
|
62 MLTEXT="" |
|
63 MODES="" |
|
64 TERMINATE="" |
|
65 READONLY="" |
|
66 NOWRITE="" |
|
67 |
|
68 while getopts "CIPce:fm:qruw" OPT |
|
69 do |
|
70 case "$OPT" in |
|
71 C) |
|
72 COPYDB=true |
|
73 ;; |
|
74 I) |
|
75 ISAR=true |
|
76 ;; |
|
77 P) |
|
78 PROOFGENERAL=true |
|
79 ;; |
|
80 c) |
|
81 COMPRESS=true |
|
82 ;; |
|
83 e) |
|
84 MLTEXT="$MLTEXT $OPTARG" |
|
85 ;; |
|
86 f) |
|
87 MLTEXT="$MLTEXT Session.finish();" |
|
88 ;; |
|
89 m) |
|
90 if [ -z "$MODES" ]; then |
|
91 MODES="\"$OPTARG\"" |
|
92 else |
|
93 MODES="\"$OPTARG\", $MODES" |
|
94 fi |
|
95 ;; |
|
96 q) |
|
97 TERMINATE=true |
|
98 ;; |
|
99 r) |
|
100 READONLY=true |
|
101 ;; |
|
102 u) |
|
103 MLTEXT="$MLTEXT use\"ROOT.ML\";" |
|
104 ;; |
|
105 w) |
|
106 NOWRITE=true |
|
107 ;; |
|
108 \?) |
|
109 usage |
|
110 ;; |
|
111 esac |
|
112 done |
|
113 |
|
114 shift $(($OPTIND - 1)) |
|
115 |
|
116 |
|
117 # args |
|
118 |
|
119 INPUT="" |
|
120 OUTPUT="" |
|
121 |
|
122 if [ "$#" -ge 1 ]; then |
|
123 INPUT="$1" |
|
124 shift |
|
125 fi |
|
126 |
|
127 if [ "$#" -ge 1 ]; then |
|
128 OUTPUT="$1" |
|
129 shift |
|
130 fi |
|
131 |
|
132 [ "$#" -ne 0 ] && { echo "Bad args: $*"; usage; } |
|
133 |
|
134 |
|
135 ## check ML system |
|
136 |
|
137 [ -z "$ML_SYSTEM" ] && fail "Missing ML system settings! Unable to run Isabelle." |
|
138 |
|
139 |
|
140 ## input heap file |
|
141 |
|
142 [ -z "$INPUT" ] && INPUT="$ISABELLE_LOGIC" |
|
143 |
|
144 case "$INPUT" in |
|
145 RAW_ML_SYSTEM) |
|
146 INFILE="" |
|
147 ;; |
|
148 */*) |
|
149 INFILE="$INPUT" |
|
150 [ ! -f "$INFILE" ] && fail "Bad heap file: \"$INFILE\"" |
|
151 ;; |
|
152 *) |
|
153 INFILE="" |
|
154 ISA_PATH="" |
|
155 |
|
156 ORIG_IFS="$IFS" |
|
157 IFS=":" |
|
158 for DIR in $ISABELLE_PATH |
|
159 do |
|
160 DIR="$DIR/$ML_IDENTIFIER" |
|
161 ISA_PATH="$ISA_PATH $DIR\n" |
|
162 [ -z "$INFILE" -a -f "$DIR/$INPUT" ] && INFILE="$DIR/$INPUT" |
|
163 done |
|
164 IFS="$ORIG_IFS" |
|
165 |
|
166 if [ -z "$INFILE" ]; then |
|
167 echo "Unknown logic \"$INPUT\" -- no heap file found in:" >&2 |
|
168 echo -ne "$ISA_PATH" >&2 |
|
169 exit 2 |
|
170 fi |
|
171 ;; |
|
172 esac |
|
173 |
|
174 |
|
175 ## output heap file |
|
176 |
|
177 case "$OUTPUT" in |
|
178 "") |
|
179 [ -z "$READONLY" -a -w "$INFILE" ] && OUTFILE="$INFILE" |
|
180 ;; |
|
181 */*) |
|
182 OUTFILE="$OUTPUT" |
|
183 ;; |
|
184 *) |
|
185 mkdir -p "$ISABELLE_OUTPUT" |
|
186 OUTFILE="$ISABELLE_OUTPUT/$OUTPUT" |
|
187 ;; |
|
188 esac |
|
189 |
|
190 |
|
191 ## prepare tmp directory |
|
192 |
|
193 [ -z "$ISABELLE_TMP_PREFIX" ] && ISABELLE_TMP_PREFIX=/tmp/isabelle |
|
194 |
|
195 ISABELLE_TMP="$ISABELLE_TMP_PREFIX$$" |
|
196 mkdir -p "$ISABELLE_TMP" |
|
197 |
|
198 |
|
199 ## run it! |
|
200 |
|
201 ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-) |
|
202 |
|
203 [ -n "$MODES" ] && MLTEXT="print_mode := [$MODES]; $MLTEXT" |
|
204 |
|
205 if [ -n "$PROOFGENERAL" ]; then |
|
206 MLTEXT="$MLTEXT; ProofGeneral.init $ISAR;" |
|
207 elif [ "$ISAR" = true ]; then |
|
208 MLTEXT="$MLTEXT; Isar.main();" |
|
209 fi |
|
210 |
|
211 export INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE ISABELLE_TMP |
|
212 |
|
213 if [ -f "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" ]; then |
|
214 "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" |
|
215 else |
|
216 "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE" |
|
217 fi |
|
218 RC="$?" |
|
219 |
|
220 #Do not even think of 'rm -r'!! |
|
221 rmdir "$ISABELLE_TMP" |
|
222 |
|
223 exit "$RC" |
|