wenzelm@10014
|
1 |
#!/bin/bash
|
wenzelm@6485
|
2 |
#
|
wenzelm@6485
|
3 |
# $Id$
|
wenzelm@6485
|
4 |
#
|
wenzelm@6485
|
5 |
# makerpm -- make Isabelle rpm packages for Linux/x86 from the distribution.
|
wenzelm@6485
|
6 |
|
wenzelm@6485
|
7 |
|
wenzelm@6485
|
8 |
## global settings
|
wenzelm@6485
|
9 |
|
wenzelm@8853
|
10 |
FAKE_BUILD=""
|
wenzelm@6485
|
11 |
DISTBASE=~/tmp/isadist
|
wenzelm@6499
|
12 |
ROOT=/usr/share
|
wenzelm@6499
|
13 |
BIN=/usr/bin
|
wenzelm@9925
|
14 |
RPMRELEASE=1
|
wenzelm@6485
|
15 |
|
wenzelm@6485
|
16 |
|
wenzelm@6485
|
17 |
## diagnostics
|
wenzelm@6485
|
18 |
|
wenzelm@9925
|
19 |
PRG=$(basename "$0")
|
wenzelm@6485
|
20 |
|
wenzelm@6485
|
21 |
function usage()
|
wenzelm@6485
|
22 |
{
|
wenzelm@6485
|
23 |
echo
|
wenzelm@6485
|
24 |
echo "Usage: $PRG ARCHIVE"
|
wenzelm@6485
|
25 |
echo
|
wenzelm@7488
|
26 |
echo "Make Isabelle rpm packages for Linux/x86 from the distribution archives."
|
wenzelm@6485
|
27 |
echo
|
wenzelm@6485
|
28 |
exit 1
|
wenzelm@6485
|
29 |
}
|
wenzelm@6485
|
30 |
|
wenzelm@6485
|
31 |
function fail()
|
wenzelm@6485
|
32 |
{
|
wenzelm@6485
|
33 |
echo "$1" >&2
|
wenzelm@6485
|
34 |
exit 2
|
wenzelm@6485
|
35 |
}
|
wenzelm@6485
|
36 |
|
wenzelm@6485
|
37 |
|
wenzelm@6485
|
38 |
## process command line
|
wenzelm@6485
|
39 |
|
wenzelm@9925
|
40 |
[ "$#" -gt 1 ] && usage
|
wenzelm@6485
|
41 |
|
wenzelm@7488
|
42 |
ARCHIVE="$1"; shift
|
wenzelm@7488
|
43 |
|
wenzelm@6485
|
44 |
|
wenzelm@6485
|
45 |
|
wenzelm@6485
|
46 |
## main
|
wenzelm@6485
|
47 |
|
wenzelm@6485
|
48 |
[ ! -f "$ARCHIVE" ] && fail "Bad archive file $ARCHIVE"
|
wenzelm@6485
|
49 |
ARCHIVE_BASE=$(basename "$ARCHIVE")
|
wenzelm@9925
|
50 |
ARCHIVE_DIR=$(cd $(dirname "$ARCHIVE"); echo "$PWD")
|
wenzelm@7488
|
51 |
ARCHIVE_FULL=$ARCHIVE_DIR/$ARCHIVE_BASE
|
wenzelm@6485
|
52 |
|
wenzelm@6485
|
53 |
ISABELLE_NAME=$(basename "$ARCHIVE_BASE" .tar.gz)
|
wenzelm@6485
|
54 |
ISABELLE_HOME="$ROOT/$ISABELLE_NAME"
|
wenzelm@6485
|
55 |
|
wenzelm@7488
|
56 |
PDF_ARCHIVE_FULL="$ARCHIVE_DIR/${ISABELLE_NAME}_pdf.tar.gz"
|
wenzelm@7488
|
57 |
[ ! -f "$PDF_ARCHIVE_FULL" ] && PDF_ARCHIVE_FULL=""
|
wenzelm@7488
|
58 |
|
wenzelm@6485
|
59 |
|
wenzelm@6485
|
60 |
# prep
|
wenzelm@6485
|
61 |
|
wenzelm@6485
|
62 |
TMP="/tmp/isabelle-makerpm$$"
|
wenzelm@6485
|
63 |
for D in "BUILD$ROOT" RPMS/i386 SOURCES SPECS SRPMS; do mkdir -p "$TMP/$D"; done
|
wenzelm@6485
|
64 |
|
wenzelm@6485
|
65 |
cd "$TMP/BUILD$ROOT"
|
wenzelm@6485
|
66 |
tar -xpzf "$ARCHIVE_FULL"
|
wenzelm@7488
|
67 |
[ -n "$PDF_ARCHIVE_FULL" ] && tar -xpzf "$PDF_ARCHIVE_FULL"
|
wenzelm@6485
|
68 |
|
wenzelm@6485
|
69 |
|
wenzelm@6485
|
70 |
# build
|
wenzelm@6485
|
71 |
|
wenzelm@6485
|
72 |
cd "$TMP/BUILD$ROOT/$ISABELLE_NAME"
|
wenzelm@7488
|
73 |
( env BASH_PATH=/bin/bash PERL_PATH=/usr/bin/perl ./configure )
|
wenzelm@6485
|
74 |
COMPILER=$(./bin/isatool getenv -b ML_IDENTIFIER)
|
wenzelm@6485
|
75 |
|
wenzelm@8853
|
76 |
if [ -n "$FAKE_BUILD" ]; then
|
wenzelm@8853
|
77 |
mkdir -p heaps/${COMPILER}
|
wenzelm@8853
|
78 |
touch heaps/${COMPILER}/HOL
|
wenzelm@8853
|
79 |
touch heaps/${COMPILER}/HOL-Real
|
wenzelm@8853
|
80 |
touch heaps/${COMPILER}/ZF
|
wenzelm@8853
|
81 |
else
|
wenzelm@10039
|
82 |
./build -b -m HOL-Real HOL
|
wenzelm@10039
|
83 |
./build -b ZF
|
wenzelm@8853
|
84 |
rm -f heaps/${COMPILER}/Pure heaps/${COMPILER}/FOL heaps/${COMPILER}/TLA
|
wenzelm@8853
|
85 |
fi
|
wenzelm@8046
|
86 |
|
wenzelm@6485
|
87 |
|
wenzelm@6485
|
88 |
# rpm spec
|
wenzelm@6485
|
89 |
|
wenzelm@6485
|
90 |
RPMVERSION=$(echo "$ISABELLE_NAME" | perl -w \
|
wenzelm@6485
|
91 |
-e '$name = <STDIN>;' \
|
wenzelm@6485
|
92 |
-e 'if ($name =~ m/^Isabelle(\d+)$/) {' \
|
wenzelm@6485
|
93 |
-e ' $rpmversion = "$1";' \
|
wenzelm@6485
|
94 |
-e '} elsif ($name =~ m/^Isabelle(\d+)-(\d+)$/) {' \
|
wenzelm@6485
|
95 |
-e ' $rpmversion = "$1p$2";' \
|
wenzelm@6485
|
96 |
-e '} elsif ($name =~ m/^Isabelle_(\d+)-(\w+)-(\d+)$/) {' \
|
wenzelm@6485
|
97 |
-e ' $rpmversion = "$1$2$3";' \
|
wenzelm@6485
|
98 |
-e '} else {' \
|
wenzelm@6485
|
99 |
-e ' $rpmversion = "";' \
|
wenzelm@6485
|
100 |
-e '};' \
|
wenzelm@6485
|
101 |
-e 'print $rpmversion;')
|
wenzelm@6485
|
102 |
|
wenzelm@6485
|
103 |
[ -z "$RPMVERSION" ] && fail "Unable to derive package version from $ISABELLE_NAME"
|
wenzelm@6485
|
104 |
|
wenzelm@6485
|
105 |
cat >$TMP/SPECS/isabelle.spec <<EOF
|
wenzelm@6485
|
106 |
Summary: Isabelle Theorem Proving Environment
|
wenzelm@6485
|
107 |
Name: isabelle
|
wenzelm@6485
|
108 |
Version: $RPMVERSION
|
wenzelm@7992
|
109 |
Release: $RPMRELEASE
|
wenzelm@6485
|
110 |
Group: Applications/Math
|
wenzelm@6485
|
111 |
Copyright: University of Cambridge Computer Laboratory
|
wenzelm@6485
|
112 |
Url: http://www.cl.cam.ac.uk/Research/HVG/Isabelle/
|
wenzelm@6485
|
113 |
Packager: Markus Wenzel <wenzelm@in.tum.de>
|
wenzelm@7312
|
114 |
Prefix: $ROOT
|
wenzelm@6485
|
115 |
BuildRoot: $TMP/BUILD
|
wenzelm@6485
|
116 |
|
wenzelm@6485
|
117 |
%description
|
wenzelm@6485
|
118 |
|
wenzelm@6485
|
119 |
This package contains the full source distribution of Isabelle
|
wenzelm@6485
|
120 |
together with documentation. To make it actually run you still need
|
wenzelm@8317
|
121 |
the ML compiler and any of the precompiled Isabelle object-logics
|
wenzelm@8317
|
122 |
(e.g. package isabelle-HOL).
|
wenzelm@6485
|
123 |
|
wenzelm@6485
|
124 |
Isabelle is a popular generic theorem proving environment developed at
|
wenzelm@6485
|
125 |
Cambridge University (Larry Paulson) and TU Munich (Tobias Nipkow).
|
wenzelm@6485
|
126 |
The system can be viewed from two main perspectives. On the one hand
|
wenzelm@6485
|
127 |
it may serve as a generic framework for rapid prototyping of deductive
|
wenzelm@6485
|
128 |
systems. On the other hand, major existing logics like Isabelle/HOL
|
wenzelm@6485
|
129 |
provide a theorem proving environment ready to use for sizable
|
wenzelm@6485
|
130 |
applications.
|
wenzelm@6485
|
131 |
|
wenzelm@6485
|
132 |
The Isabelle distribution includes a large body of object logics and
|
wenzelm@6485
|
133 |
other examples (see also the Isabelle theory library at
|
wenzelm@6485
|
134 |
http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/). Isabelle/HOL
|
wenzelm@6485
|
135 |
is a version of classical higher-order logic resembling that of the
|
wenzelm@6485
|
136 |
HOL System. Isabelle/HOLCF adds Scott's Logic for Computable
|
wenzelm@6485
|
137 |
Functions (domain theory) to HOL. Isabelle/FOL provides basic
|
wenzelm@6485
|
138 |
classical and intuitionistic first-order logic. It is polymorphic.
|
wenzelm@6485
|
139 |
Isabelle/ZF offers a formulation of Zermelo-Fraenkel set theory on top
|
wenzelm@6485
|
140 |
of FOL.
|
wenzelm@6485
|
141 |
|
wenzelm@6485
|
142 |
Isabelle/HOL is currently the best developed object logic, including
|
wenzelm@6485
|
143 |
an extensive library of (concrete) mathematics, and various packages
|
wenzelm@6485
|
144 |
for advanced definitional concepts (like (co-)inductive sets and
|
wenzelm@6485
|
145 |
types, well-founded recursion etc.). The distribution also includes
|
wenzelm@6485
|
146 |
some large applications, for example correctness proofs of
|
wenzelm@6485
|
147 |
cryptographic protocols (HOL/Auth) or communication protocols
|
wenzelm@6485
|
148 |
(HOLCF/IOA).
|
wenzelm@6485
|
149 |
|
wenzelm@6485
|
150 |
Isabelle/ZF provides another starting point for applications, with a
|
wenzelm@6485
|
151 |
slightly less developed library. Its definitional packages are
|
wenzelm@6485
|
152 |
similar to those of Isabelle/HOL. Untyped ZF provides more advanced
|
wenzelm@6485
|
153 |
constructions for sets than simply-typed HOL.
|
wenzelm@6485
|
154 |
|
wenzelm@6485
|
155 |
Logics are not hard-wired into Isabelle, but formulated within
|
wenzelm@6485
|
156 |
Isabelle's meta logic: Isabelle/Pure. There are quite a lot of
|
wenzelm@6485
|
157 |
syntactic and deductive tools available in generic Isabelle. Isabelle
|
wenzelm@6485
|
158 |
proof tools provide a high degree of automation.
|
wenzelm@6485
|
159 |
|
wenzelm@10039
|
160 |
By virtue of the Isabelle/Isar subsystem, interactive proof
|
wenzelm@10039
|
161 |
development may be performed both via traditional tactic scripts, or
|
wenzelm@10039
|
162 |
actual human readable (formal) proof texts. The resulting theory
|
wenzelm@10039
|
163 |
developments may be presented in high quality as (PDF)LaTeX documents,
|
wenzelm@10039
|
164 |
accommodating both printed copies and WWW browsing.
|
wenzelm@10039
|
165 |
|
wenzelm@6485
|
166 |
%package HOL
|
wenzelm@6485
|
167 |
Summary: Isabelle Theorem Proving Environment -- Higher-Order Logic
|
wenzelm@6485
|
168 |
Group: Applications/Math
|
wenzelm@6567
|
169 |
Requires: isabelle
|
wenzelm@6485
|
170 |
%description HOL
|
wenzelm@6485
|
171 |
This package contains a binary image of the HOL object-logic for Isabelle.
|
wenzelm@6485
|
172 |
|
wenzelm@7312
|
173 |
%package HOL-Real
|
wenzelm@7312
|
174 |
Summary: Isabelle Theorem Proving Environment -- Higher-Order Logic
|
wenzelm@7312
|
175 |
Group: Applications/Math
|
wenzelm@7312
|
176 |
Requires: isabelle
|
wenzelm@7312
|
177 |
%description HOL-Real
|
wenzelm@7312
|
178 |
This package contains a binary image of the HOL object-logic for Isabelle,
|
wenzelm@7312
|
179 |
including support for real numbers.
|
wenzelm@7312
|
180 |
|
wenzelm@6485
|
181 |
%package ZF
|
wenzelm@6485
|
182 |
Summary: Isabelle Theorem Proving Environment -- Zermelo-Fraenkel set theory
|
wenzelm@6485
|
183 |
Group: Applications/Math
|
wenzelm@6567
|
184 |
Requires: isabelle
|
wenzelm@6485
|
185 |
%description ZF
|
wenzelm@6485
|
186 |
This package contains a binary image of the ZF object-logic for Isabelle.
|
wenzelm@6485
|
187 |
|
wenzelm@7488
|
188 |
%package pdfdocs
|
wenzelm@7488
|
189 |
Summary: Isabelle Theorem Proving Environment -- PDF documentation
|
wenzelm@7488
|
190 |
Group: Applications/Math
|
wenzelm@7488
|
191 |
Requires: isabelle
|
wenzelm@7488
|
192 |
%description pdfdocs
|
wenzelm@7488
|
193 |
This package contains the Isabelle documentation in PDF. Note that
|
wenzelm@7488
|
194 |
the dvi version is already part of the base package.
|
wenzelm@7488
|
195 |
|
wenzelm@6485
|
196 |
%prep
|
wenzelm@6485
|
197 |
|
wenzelm@6485
|
198 |
%build
|
wenzelm@6485
|
199 |
|
wenzelm@6485
|
200 |
%install
|
wenzelm@6485
|
201 |
|
wenzelm@7312
|
202 |
%post
|
wenzelm@7312
|
203 |
\$RPM_INSTALL_PREFIX/$ISABELLE_NAME/bin/isatool install -p $BIN
|
wenzelm@7312
|
204 |
|
wenzelm@7312
|
205 |
%post HOL
|
wenzelm@7312
|
206 |
%post HOL-Real
|
wenzelm@7312
|
207 |
%post ZF
|
wenzelm@7488
|
208 |
%post pdfdocs
|
wenzelm@7312
|
209 |
|
wenzelm@7312
|
210 |
%postun
|
wenzelm@7312
|
211 |
rm -f $BIN/Isabelle $BIN/isabelle $BIN/isatool
|
wenzelm@7312
|
212 |
|
wenzelm@7312
|
213 |
%postun HOL
|
wenzelm@7312
|
214 |
%postun HOL-Real
|
wenzelm@7312
|
215 |
%postun ZF
|
wenzelm@7488
|
216 |
%postun pdfdocs
|
wenzelm@7312
|
217 |
|
wenzelm@7312
|
218 |
|
wenzelm@6485
|
219 |
%files HOL
|
wenzelm@6485
|
220 |
$ISABELLE_HOME/heaps/${COMPILER}/HOL
|
wenzelm@6485
|
221 |
|
wenzelm@7312
|
222 |
%files HOL-Real
|
wenzelm@7312
|
223 |
$ISABELLE_HOME/heaps/${COMPILER}/HOL-Real
|
wenzelm@7312
|
224 |
|
wenzelm@6485
|
225 |
%files ZF
|
wenzelm@6485
|
226 |
$ISABELLE_HOME/heaps/${COMPILER}/ZF
|
wenzelm@6485
|
227 |
|
wenzelm@7488
|
228 |
%files pdfdocs
|
wenzelm@7488
|
229 |
EOF
|
wenzelm@7488
|
230 |
|
wenzelm@7488
|
231 |
for F in $(ls -1 doc/*.pdf); do
|
wenzelm@7488
|
232 |
echo "$ISABELLE_HOME/$F" >>$TMP/SPECS/isabelle.spec
|
wenzelm@7488
|
233 |
done
|
wenzelm@7488
|
234 |
|
wenzelm@7488
|
235 |
|
wenzelm@7488
|
236 |
cat >>$TMP/SPECS/isabelle.spec <<EOF
|
wenzelm@6485
|
237 |
%files
|
wenzelm@7337
|
238 |
%dir $ISABELLE_HOME
|
wenzelm@7488
|
239 |
%dir $ISABELLE_HOME/doc
|
wenzelm@7337
|
240 |
%dir $ISABELLE_HOME/heaps
|
wenzelm@7337
|
241 |
%dir $ISABELLE_HOME/heaps/${COMPILER}
|
wenzelm@6485
|
242 |
EOF
|
wenzelm@6485
|
243 |
|
wenzelm@7488
|
244 |
for F in $(ls -1 | grep -v heaps | grep -v browser_info | grep -v doc); do
|
wenzelm@7488
|
245 |
echo "$ISABELLE_HOME/$F" >>$TMP/SPECS/isabelle.spec
|
wenzelm@7488
|
246 |
done
|
wenzelm@7488
|
247 |
|
wenzelm@7488
|
248 |
for F in $(ls -1 doc/* | grep -v pdf); do
|
wenzelm@6485
|
249 |
echo "$ISABELLE_HOME/$F" >>$TMP/SPECS/isabelle.spec
|
wenzelm@6485
|
250 |
done
|
wenzelm@6485
|
251 |
|
wenzelm@6485
|
252 |
|
wenzelm@6485
|
253 |
# invoke rpm
|
wenzelm@6485
|
254 |
|
wenzelm@6561
|
255 |
chown -R root:root "$TMP" || chgrp -R isabelle "$TMP"
|
wenzelm@6495
|
256 |
|
wenzelm@8046
|
257 |
rpm -bb "$TMP/SPECS/isabelle.spec"
|
wenzelm@6485
|
258 |
|
wenzelm@6485
|
259 |
mkdir -p "$DISTBASE/rpm"
|
wenzelm@8046
|
260 |
cd /usr/src/packages/RPMS/i386
|
wenzelm@8046
|
261 |
mv "isabelle-$RPMVERSION-${RPMRELEASE}.i386.rpm" "$DISTBASE/rpm/isabelle.rpm"
|
wenzelm@8046
|
262 |
mv "isabelle-HOL-$RPMVERSION-${RPMRELEASE}.i386.rpm" "$DISTBASE/rpm/isabelle-HOL.i386.rpm"
|
wenzelm@8046
|
263 |
mv "isabelle-HOL-Real-$RPMVERSION-${RPMRELEASE}.i386.rpm" "$DISTBASE/rpm/isabelle-HOL-Real.i386.rpm"
|
wenzelm@8046
|
264 |
mv "isabelle-ZF-$RPMVERSION-${RPMRELEASE}.i386.rpm" "$DISTBASE/rpm/isabelle-ZF.i386.rpm"
|
wenzelm@8046
|
265 |
mv "isabelle-pdfdocs-$RPMVERSION-${RPMRELEASE}.i386.rpm" "$DISTBASE/rpm/isabelle-pdfdocs.rpm"
|
wenzelm@6485
|
266 |
|
wenzelm@6485
|
267 |
# clean up
|
wenzelm@6485
|
268 |
cd /
|
wenzelm@6485
|
269 |
rm -rf "$TMP"
|