#!/bin/bash
#
# $Id$
#
# makerpm -- make Isabelle rpm packages for Linux/x86 from the distribution.
## global settings
LOGICS="HOL ZF"
DISTBASE=~/tmp/isadist
ROOT=/usr/share
BIN=/usr/bin
RPMRELEASE=2
## diagnostics
PRG=$(basename $0)
function usage()
{
echo
echo "Usage: $PRG ARCHIVE"
echo
echo "Make Isabelle rpm packages for Linux/x86 from the distribution archives."
echo
exit 1
}
function fail()
{
echo "$1" >&2
exit 2
}
## process command line
[ $# -gt 1 ] && usage
ARCHIVE="$1"; shift
## main
[ ! -f "$ARCHIVE" ] && fail "Bad archive file $ARCHIVE"
ARCHIVE_BASE=$(basename "$ARCHIVE")
ARCHIVE_DIR=$(cd $(dirname "$ARCHIVE"); echo $PWD)
ARCHIVE_FULL=$ARCHIVE_DIR/$ARCHIVE_BASE
ISABELLE_NAME=$(basename "$ARCHIVE_BASE" .tar.gz)
ISABELLE_HOME="$ROOT/$ISABELLE_NAME"
PDF_ARCHIVE_FULL="$ARCHIVE_DIR/${ISABELLE_NAME}_pdf.tar.gz"
[ ! -f "$PDF_ARCHIVE_FULL" ] && PDF_ARCHIVE_FULL=""
# prep
TMP="/tmp/isabelle-makerpm$$"
for D in "BUILD$ROOT" RPMS/i386 SOURCES SPECS SRPMS; do mkdir -p "$TMP/$D"; done
cd "$TMP/BUILD$ROOT"
tar -xpzf "$ARCHIVE_FULL"
[ -n "$PDF_ARCHIVE_FULL" ] && tar -xpzf "$PDF_ARCHIVE_FULL"
# build
cd "$TMP/BUILD$ROOT/$ISABELLE_NAME"
( env BASH_PATH=/bin/bash PERL_PATH=/usr/bin/perl ./configure )
./build -bi $LOGICS
COMPILER=$(./bin/isatool getenv -b ML_IDENTIFIER)
rm -f heaps/${COMPILER}/Pure heaps/${COMPILER}/FOL heaps/${COMPILER}/TLA
# fake build
#mkdir -p heaps/${COMPILER}
#touch heaps/${COMPILER}/HOL
#touch heaps/${COMPILER}/HOL-Real
#touch heaps/${COMPILER}/ZF
# rpm spec
RPMVERSION=$(echo "$ISABELLE_NAME" | perl -w \
-e '$name = <STDIN>;' \
-e 'if ($name =~ m/^Isabelle(\d+)$/) {' \
-e ' $rpmversion = "$1";' \
-e '} elsif ($name =~ m/^Isabelle(\d+)-(\d+)$/) {' \
-e ' $rpmversion = "$1p$2";' \
-e '} elsif ($name =~ m/^Isabelle_(\d+)-(\w+)-(\d+)$/) {' \
-e ' $rpmversion = "$1$2$3";' \
-e '} else {' \
-e ' $rpmversion = "";' \
-e '};' \
-e 'print $rpmversion;')
[ -z "$RPMVERSION" ] && fail "Unable to derive package version from $ISABELLE_NAME"
cat >$TMP/SPECS/isabelle.spec <<EOF
Summary: Isabelle Theorem Proving Environment
Name: isabelle
Version: $RPMVERSION
Release: $RPMRELEASE
Group: Applications/Math
Copyright: University of Cambridge Computer Laboratory
Url: http://www.cl.cam.ac.uk/Research/HVG/Isabelle/
Packager: Markus Wenzel <wenzelm@in.tum.de>
Prefix: $ROOT
BuildRoot: $TMP/BUILD
%description
This package contains the full source distribution of Isabelle
together with documentation. To make it actually run you still need
the ML compiler and any of the precompiled Isabelle object-logics
(e.g. package isabelle-HOL).
Isabelle is a popular generic theorem proving environment developed at
Cambridge University (Larry Paulson) and TU Munich (Tobias Nipkow).
The system can be viewed from two main perspectives. On the one hand
it may serve as a generic framework for rapid prototyping of deductive
systems. On the other hand, major existing logics like Isabelle/HOL
provide a theorem proving environment ready to use for sizable
applications.
The Isabelle distribution includes a large body of object logics and
other examples (see also the Isabelle theory library at
http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/). Isabelle/HOL
is a version of classical higher-order logic resembling that of the
HOL System. Isabelle/HOLCF adds Scott's Logic for Computable
Functions (domain theory) to HOL. Isabelle/FOL provides basic
classical and intuitionistic first-order logic. It is polymorphic.
Isabelle/ZF offers a formulation of Zermelo-Fraenkel set theory on top
of FOL.
Isabelle/HOL is currently the best developed object logic, including
an extensive library of (concrete) mathematics, and various packages
for advanced definitional concepts (like (co-)inductive sets and
types, well-founded recursion etc.). The distribution also includes
some large applications, for example correctness proofs of
cryptographic protocols (HOL/Auth) or communication protocols
(HOLCF/IOA).
Isabelle/ZF provides another starting point for applications, with a
slightly less developed library. Its definitional packages are
similar to those of Isabelle/HOL. Untyped ZF provides more advanced
constructions for sets than simply-typed HOL.
Logics are not hard-wired into Isabelle, but formulated within
Isabelle's meta logic: Isabelle/Pure. There are quite a lot of
syntactic and deductive tools available in generic Isabelle. Isabelle
proof tools provide a high degree of automation.
%package HOL
Summary: Isabelle Theorem Proving Environment -- Higher-Order Logic
Group: Applications/Math
Requires: isabelle
%description HOL
This package contains a binary image of the HOL object-logic for Isabelle.
%package HOL-Real
Summary: Isabelle Theorem Proving Environment -- Higher-Order Logic
Group: Applications/Math
Requires: isabelle
%description HOL-Real
This package contains a binary image of the HOL object-logic for Isabelle,
including support for real numbers.
%package ZF
Summary: Isabelle Theorem Proving Environment -- Zermelo-Fraenkel set theory
Group: Applications/Math
Requires: isabelle
%description ZF
This package contains a binary image of the ZF object-logic for Isabelle.
%package pdfdocs
Summary: Isabelle Theorem Proving Environment -- PDF documentation
Group: Applications/Math
Requires: isabelle
%description pdfdocs
This package contains the Isabelle documentation in PDF. Note that
the dvi version is already part of the base package.
%prep
%build
%install
%post
\$RPM_INSTALL_PREFIX/$ISABELLE_NAME/bin/isatool install -p $BIN
%post HOL
%post HOL-Real
%post ZF
%post pdfdocs
%postun
rm -f $BIN/Isabelle $BIN/isabelle $BIN/isatool
%postun HOL
%postun HOL-Real
%postun ZF
%postun pdfdocs
%files HOL
$ISABELLE_HOME/heaps/${COMPILER}/HOL
%files HOL-Real
$ISABELLE_HOME/heaps/${COMPILER}/HOL-Real
%files ZF
$ISABELLE_HOME/heaps/${COMPILER}/ZF
%files pdfdocs
EOF
for F in $(ls -1 doc/*.pdf); do
echo "$ISABELLE_HOME/$F" >>$TMP/SPECS/isabelle.spec
done
cat >>$TMP/SPECS/isabelle.spec <<EOF
%files
%dir $ISABELLE_HOME
%dir $ISABELLE_HOME/doc
%dir $ISABELLE_HOME/heaps
%dir $ISABELLE_HOME/heaps/${COMPILER}
EOF
for F in $(ls -1 | grep -v heaps | grep -v browser_info | grep -v doc); do
echo "$ISABELLE_HOME/$F" >>$TMP/SPECS/isabelle.spec
done
for F in $(ls -1 doc/* | grep -v pdf); do
echo "$ISABELLE_HOME/$F" >>$TMP/SPECS/isabelle.spec
done
# invoke rpm
chown -R root:root "$TMP" || chgrp -R isabelle "$TMP"
rpm -bb "$TMP/SPECS/isabelle.spec"
mkdir -p "$DISTBASE/rpm"
cd /usr/src/packages/RPMS/i386
mv "isabelle-$RPMVERSION-${RPMRELEASE}.i386.rpm" "$DISTBASE/rpm/isabelle.rpm"
mv "isabelle-HOL-$RPMVERSION-${RPMRELEASE}.i386.rpm" "$DISTBASE/rpm/isabelle-HOL.i386.rpm"
mv "isabelle-HOL-Real-$RPMVERSION-${RPMRELEASE}.i386.rpm" "$DISTBASE/rpm/isabelle-HOL-Real.i386.rpm"
mv "isabelle-ZF-$RPMVERSION-${RPMRELEASE}.i386.rpm" "$DISTBASE/rpm/isabelle-ZF.i386.rpm"
mv "isabelle-pdfdocs-$RPMVERSION-${RPMRELEASE}.i386.rpm" "$DISTBASE/rpm/isabelle-pdfdocs.rpm"
# clean up
cd /
rm -rf "$TMP"