1 #!/usr/bin/env bash |
|
2 # |
|
3 # Author: Markus Wenzel, TU Muenchen |
|
4 # |
|
5 # DESCRIPTION: prepare logic session directory |
|
6 |
|
7 |
|
8 ## diagnostics |
|
9 |
|
10 PRG="$(basename "$0")" |
|
11 |
|
12 function usage() |
|
13 { |
|
14 echo |
|
15 echo "Usage: isabelle $PRG [OPTIONS] [LOGIC] NAME" |
|
16 echo |
|
17 echo " Options are:" |
|
18 echo " -I FILE alternative IsaMakefile output" |
|
19 echo " -P include parent logic target" |
|
20 echo " -b setup build mode (session outputs heap image)" |
|
21 echo " -q quiet mode" |
|
22 echo |
|
23 echo " Prepare session directory, including IsaMakefile and document source" |
|
24 echo " with parent LOGIC (default ISABELLE_LOGIC=$ISABELLE_LOGIC)" |
|
25 echo |
|
26 exit 1 |
|
27 } |
|
28 |
|
29 function fail() |
|
30 { |
|
31 echo "$1" >&2 |
|
32 exit 2 |
|
33 } |
|
34 |
|
35 |
|
36 ## process command line |
|
37 |
|
38 # options |
|
39 |
|
40 ISAMAKEFILE="IsaMakefile" |
|
41 PARENT="" |
|
42 BUILD="" |
|
43 QUIET="" |
|
44 |
|
45 while getopts "I:Pbq" OPT |
|
46 do |
|
47 case "$OPT" in |
|
48 I) |
|
49 ISAMAKEFILE="$OPTARG" |
|
50 ;; |
|
51 P) |
|
52 PARENT=true |
|
53 ;; |
|
54 b) |
|
55 BUILD=true |
|
56 ;; |
|
57 q) |
|
58 QUIET=true |
|
59 ;; |
|
60 \?) |
|
61 usage |
|
62 ;; |
|
63 esac |
|
64 done |
|
65 |
|
66 shift $(($OPTIND - 1)) |
|
67 |
|
68 |
|
69 # args |
|
70 |
|
71 |
|
72 if [ "$#" -eq 1 ]; then |
|
73 LOGIC="$ISABELLE_LOGIC" |
|
74 DIR_NAME="$1"; shift |
|
75 elif [ "$#" -eq 2 ]; then |
|
76 LOGIC="$1"; shift |
|
77 DIR_NAME="$1"; shift |
|
78 else |
|
79 usage |
|
80 fi |
|
81 |
|
82 DIR=$(dirname "$DIR_NAME") |
|
83 NAME=$(basename "$DIR_NAME") |
|
84 |
|
85 |
|
86 ## main |
|
87 |
|
88 [ -z "$QUIET" ] && echo "Preparing session \"$NAME\" ..." |
|
89 |
|
90 |
|
91 # IsaMakefile |
|
92 |
|
93 mkdir -p "$DIR" || fail "Bad directory: $DIR" |
|
94 cd "$DIR" |
|
95 |
|
96 DOCUMENT_ROOT="" |
|
97 VERBOSE="" |
|
98 [ -z "$QUIET" ] && VERBOSE="-v true " |
|
99 |
|
100 if [ -n "$BUILD" ]; then |
|
101 IMAGES="$NAME" |
|
102 TEST="" |
|
103 TARGET="\$(OUT)/$NAME" |
|
104 ROOT_ML="ROOT.ML" |
|
105 SOURCES="*.thy" |
|
106 DOCUMENT_ROOT="document/root.tex" |
|
107 USEDIR="\$(USEDIR) -b -P http://isabelle.in.tum.de/library" |
|
108 else |
|
109 IMAGES="" |
|
110 TEST="$NAME" |
|
111 TARGET="\$(LOG)/$LOGIC-$NAME.gz" |
|
112 ROOT_ML="$NAME/ROOT.ML" |
|
113 SOURCES="$NAME/*.thy" |
|
114 DOCUMENT_ROOT="$NAME/document/root.tex" |
|
115 USEDIR="\$(USEDIR)" |
|
116 fi |
|
117 |
|
118 if [ "$ISAMAKEFILE" != - -a -f "$ISAMAKEFILE" ]; then |
|
119 echo "keeping $DIR/$ISAMAKEFILE" >&2 |
|
120 else |
|
121 [ -z "$QUIET" -a -n "$ISAMAKEFILE" -a "$ISAMAKEFILE" != - ] && \ |
|
122 echo "creating $DIR/$ISAMAKEFILE" >&2 |
|
123 { echo |
|
124 echo "## targets" |
|
125 echo |
|
126 echo "default: $NAME" |
|
127 echo "images: $IMAGES" |
|
128 echo "test: $TEST" |
|
129 echo |
|
130 echo "all: images test" |
|
131 echo |
|
132 echo |
|
133 echo "## global settings" |
|
134 echo |
|
135 echo "SRC = \$(ISABELLE_HOME)/src" |
|
136 echo "OUT = \$(ISABELLE_OUTPUT)" |
|
137 echo "LOG = \$(OUT)/log" |
|
138 echo |
|
139 echo "USEDIR = \$(ISABELLE_TOOL) usedir ${VERBOSE}-i true -d $ISABELLE_DOC_FORMAT ## -D generated" |
|
140 echo |
|
141 echo |
|
142 echo "## $NAME" |
|
143 echo "" |
|
144 if [ -n "$PARENT" ]; then |
|
145 echo "$NAME: $LOGIC $TARGET" |
|
146 echo |
|
147 echo "$LOGIC:" |
|
148 echo -e "\t@cd \$(SRC)/$LOGIC; \$(ISABELLE_TOOL) make $LOGIC" |
|
149 echo |
|
150 echo "$TARGET: \$(OUT)/$LOGIC $ROOT_ML $DOCUMENT_ROOT ## $SOURCES" |
|
151 echo -e "\t@$USEDIR \$(OUT)/$LOGIC $NAME" |
|
152 else |
|
153 echo "$NAME: $TARGET" |
|
154 echo |
|
155 echo "$TARGET: ## $ROOT_ML $DOCUMENT_ROOT $SOURCES" |
|
156 echo -e "\t@$USEDIR $LOGIC $NAME" |
|
157 fi |
|
158 echo |
|
159 echo |
|
160 echo "## clean" |
|
161 echo |
|
162 echo "clean:" |
|
163 echo -e "\t@rm -f $TARGET" |
|
164 } | { |
|
165 if [ -z "$ISAMAKEFILE" -o "$ISAMAKEFILE" = - ]; then |
|
166 cat |
|
167 else |
|
168 cat > "$ISAMAKEFILE" |
|
169 fi |
|
170 } |
|
171 fi |
|
172 |
|
173 |
|
174 # base directory |
|
175 |
|
176 if [ -z "$BUILD" ]; then |
|
177 mkdir -p "$NAME" || fail "Bad directory: $DIR/$NAME" |
|
178 cd "$NAME" |
|
179 PREFIX="$DIR/$NAME" |
|
180 else |
|
181 PREFIX="$DIR" |
|
182 fi |
|
183 |
|
184 if [ -f ROOT.ML ]; then |
|
185 echo "keeping $PREFIX/ROOT.ML" >&2 |
|
186 else |
|
187 [ -z "$QUIET" ] && echo "creating $PREFIX/ROOT.ML" >&2 |
|
188 cat >ROOT.ML <<EOF |
|
189 (* |
|
190 no_document use_thys ["This_Theory1", "This_Theory2"]; |
|
191 use_thys ["That_Theory1", "That_Theory2", "That_Theory3"]; |
|
192 *) |
|
193 EOF |
|
194 fi |
|
195 |
|
196 |
|
197 # document directory |
|
198 |
|
199 if [ -e document ]; then |
|
200 echo "keeping $PREFIX/document" >&2 |
|
201 else |
|
202 [ -z "$QUIET" ] && echo "creating $PREFIX/document" >&2 |
|
203 mkdir document || fail "Bad directory: $PREFIX/document" |
|
204 |
|
205 [ -z "$QUIET" ] && echo "creating $PREFIX/document/root.tex" >&2 |
|
206 TITLE=$(echo "$NAME" | tr _ - | tr -d '\\') |
|
207 AUTHOR=$(echo "By $USER" | tr _ - | tr -d '\\') |
|
208 cat >document/root.tex <<EOF |
|
209 \documentclass[11pt,a4paper]{article} |
|
210 \usepackage{isabelle,isabellesym} |
|
211 |
|
212 % further packages required for unusual symbols (see also |
|
213 % isabellesym.sty), use only when needed |
|
214 |
|
215 %\usepackage{amssymb} |
|
216 %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>, |
|
217 %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>, |
|
218 %\<triangleq>, \<yen>, \<lozenge> |
|
219 |
|
220 %\usepackage{eurosym} |
|
221 %for \<euro> |
|
222 |
|
223 %\usepackage[only,bigsqcap]{stmaryrd} |
|
224 %for \<Sqinter> |
|
225 |
|
226 %\usepackage{eufrak} |
|
227 %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb) |
|
228 |
|
229 %\usepackage{textcomp} |
|
230 %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>, |
|
231 %\<currency> |
|
232 |
|
233 % this should be the last package used |
|
234 \usepackage{pdfsetup} |
|
235 |
|
236 % urls in roman style, theory text in math-similar italics |
|
237 \urlstyle{rm} |
|
238 \isabellestyle{it} |
|
239 |
|
240 % for uniform font size |
|
241 %\renewcommand{\isastyle}{\isastyleminor} |
|
242 |
|
243 |
|
244 \begin{document} |
|
245 |
|
246 \title{$TITLE} |
|
247 \author{$AUTHOR} |
|
248 \maketitle |
|
249 |
|
250 \tableofcontents |
|
251 |
|
252 % sane default for proof documents |
|
253 \parindent 0pt\parskip 0.5ex |
|
254 |
|
255 % generated text of all theories |
|
256 \input{session} |
|
257 |
|
258 % optional bibliography |
|
259 %\bibliographystyle{abbrv} |
|
260 %\bibliography{root} |
|
261 |
|
262 \end{document} |
|
263 |
|
264 %%% Local Variables: |
|
265 %%% mode: latex |
|
266 %%% TeX-master: t |
|
267 %%% End: |
|
268 EOF |
|
269 fi |
|
270 |
|
271 |
|
272 # notes |
|
273 |
|
274 if [ -z "$QUIET" ]; then |
|
275 cat >&2 <<EOF |
|
276 |
|
277 Notes: |
|
278 |
|
279 * 'isabelle make' processes the session (including document preparation) |
|
280 |
|
281 * $DIR/IsaMakefile contains compilation options and file dependencies |
|
282 |
|
283 * $PREFIX/document/root.tex contains the LaTeX master document setup |
|
284 |
|
285 * $PREFIX/ROOT.ML needs to contain ML code to load all theories |
|
286 |
|
287 EOF |
|
288 fi |
|