|
1 #!/bin/bash |
|
2 # |
|
3 # $Id$ |
|
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: $PRG LOGIC NAME" |
|
16 echo |
|
17 echo " Options are:" |
|
18 echo " -b setup build mode (session outputs heap image)" |
|
19 echo " -d setup document" |
|
20 echo |
|
21 echo " Prepare logic session directory, including IsaMakefile, document etc." |
|
22 echo |
|
23 exit 1 |
|
24 } |
|
25 |
|
26 function fail() |
|
27 { |
|
28 echo "$1" >&2 |
|
29 exit 2 |
|
30 } |
|
31 |
|
32 |
|
33 ## process command line |
|
34 |
|
35 # options |
|
36 |
|
37 BUILD="" |
|
38 DOCUMENT="" |
|
39 |
|
40 while getopts "bd" OPT |
|
41 do |
|
42 case "$OPT" in |
|
43 b) |
|
44 BUILD=true |
|
45 ;; |
|
46 d) |
|
47 DOCUMENT=true |
|
48 ;; |
|
49 \?) |
|
50 usage |
|
51 ;; |
|
52 esac |
|
53 done |
|
54 |
|
55 shift $(($OPTIND - 1)) |
|
56 |
|
57 |
|
58 # args |
|
59 |
|
60 [ $# -ne 2 ] && usage |
|
61 |
|
62 LOGIC="$1"; shift |
|
63 NAME="$1"; shift |
|
64 |
|
65 [ -z "$SESSION" ] && SESSION=$(basename $NAME) |
|
66 |
|
67 |
|
68 |
|
69 ## main |
|
70 |
|
71 # IsaMakefile |
|
72 |
|
73 if [ -n "$BUILD" ]; then |
|
74 IMAGES="$NAME" |
|
75 TEST="" |
|
76 TARGET="\$(OUT)/$NAME" |
|
77 USEDIR="usedir -b" |
|
78 else |
|
79 IMAGES="" |
|
80 TEST="$NAME" |
|
81 TARGET="\$(LOG)/$NAME.gz" |
|
82 USEDIR="usedir" |
|
83 fi |
|
84 |
|
85 if [ -f IsaMakefile ]; then |
|
86 echo "keeping $PWD/IsaMakefile" >&2 |
|
87 else |
|
88 { echo |
|
89 echo "## targets" |
|
90 echo |
|
91 echo "default: $NAME" |
|
92 echo "images: $IMAGES" |
|
93 echo "test: $TEST" |
|
94 echo |
|
95 echo "all: images test" |
|
96 echo |
|
97 echo |
|
98 echo "## global settings" |
|
99 echo |
|
100 echo "SRC = \$(ISABELLE_HOME)/src" |
|
101 echo "OUT = \$(ISABELLE_OUTPUT)" |
|
102 echo "LOG = \$(OUT)/log" |
|
103 echo "INFO = \$(ISABELLE_BROWSER_INFO)" |
|
104 echo |
|
105 echo |
|
106 echo "## $NAME" |
|
107 echo "" |
|
108 echo "$NAME: $LOGIC $TARGET" |
|
109 echo |
|
110 echo "$LOGIC:" |
|
111 echo -e "\t@cd \$(SRC)/$LOGIC; \$(ISATOOL) make $LOGIC" |
|
112 echo |
|
113 echo "$TARGET: \$(OUT)/$LOGIC ## add $NAME sources here" |
|
114 echo -e "\t@\$(ISATOOL) $USEDIR \$(OUT)/$LOGIC $NAME" |
|
115 echo |
|
116 echo |
|
117 echo "## clean" |
|
118 echo |
|
119 echo "clean:" |
|
120 echo -e "\t@rm -f $TARGET" |
|
121 echo |
|
122 } >IsaMakefile |
|
123 fi |
|
124 |
|
125 |
|
126 # base directory |
|
127 |
|
128 if [ -z "$BUILD" ]; then |
|
129 mkdir -p "$NAME" || fail "Bad directory: $PWD/$NAME" |
|
130 cd "$NAME" |
|
131 fi |
|
132 |
|
133 if [ -f ROOT.ML ]; then |
|
134 echo "keeping $PWD/ROOT.ML" >&2 |
|
135 else |
|
136 echo -e "\n(* use_thy \"YourTheory\"; *)\n" >ROOT.ML |
|
137 fi |
|
138 |
|
139 |
|
140 # document directory |
|
141 |
|
142 if [ -n "$DOCUMENT" ]; then |
|
143 if [ -e document ]; then |
|
144 echo "keeping $PWD/document" >&2 |
|
145 else |
|
146 mkdir document || fail "Bad directory: $PWD/document" |
|
147 cat >document/root.tex <<EOF |
|
148 |
|
149 \documentclass[11pt,a4paper]{article} |
|
150 \usepackage{isabelle,isabellesym,pdfsetup} |
|
151 |
|
152 \begin{document} |
|
153 \input{session} |
|
154 \end{document} |
|
155 |
|
156 EOF |
|
157 fi |
|
158 fi |