#!/bin/bash## $Id$## makerpm -- make Isabelle rpm packages for Linux/x86 from the distribution.## global settingsLOGICS="HOL ZF"DISTBASE=~/tmp/isadistROOT=/usr/shareBIN=/usr/binRPMRELEASE=2## diagnosticsPRG=$(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 ] && usageARCHIVE="$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_BASEISABELLE_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=""# prepTMP="/tmp/isabelle-makerpm$$"for D in "BUILD$ROOT" RPMS/i386 SOURCES SPECS SRPMS; do mkdir -p "$TMP/$D"; donecd "$TMP/BUILD$ROOT"tar -xpzf "$ARCHIVE_FULL"[ -n "$PDF_ARCHIVE_FULL" ] && tar -xpzf "$PDF_ARCHIVE_FULL"# buildcd "$TMP/BUILD$ROOT/$ISABELLE_NAME"( env BASH_PATH=/bin/bash PERL_PATH=/usr/bin/perl ./configure )./build -bi $LOGICSCOMPILER=$(./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 specRPMVERSION=$(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 <<EOFSummary: Isabelle Theorem Proving EnvironmentName: isabelleVersion: $RPMVERSIONRelease: $RPMRELEASEGroup: Applications/MathCopyright: University of Cambridge Computer LaboratoryUrl: http://www.cl.cam.ac.uk/Research/HVG/Isabelle/Packager: Markus Wenzel <wenzelm@in.tum.de>Prefix: $ROOTBuildRoot: $TMP/BUILD%descriptionThis package contains the full source distribution of Isabelletogether with documentation. To make it actually run you still needthe ML compiler and any of the precompiled Isabelle object-logics(e.g. package isabelle-HOL).Isabelle is a popular generic theorem proving environment developed atCambridge University (Larry Paulson) and TU Munich (Tobias Nipkow).The system can be viewed from two main perspectives. On the one handit may serve as a generic framework for rapid prototyping of deductivesystems. On the other hand, major existing logics like Isabelle/HOLprovide a theorem proving environment ready to use for sizableapplications.The Isabelle distribution includes a large body of object logics andother examples (see also the Isabelle theory library athttp://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/). Isabelle/HOLis a version of classical higher-order logic resembling that of theHOL System. Isabelle/HOLCF adds Scott's Logic for ComputableFunctions (domain theory) to HOL. Isabelle/FOL provides basicclassical and intuitionistic first-order logic. It is polymorphic.Isabelle/ZF offers a formulation of Zermelo-Fraenkel set theory on topof FOL.Isabelle/HOL is currently the best developed object logic, includingan extensive library of (concrete) mathematics, and various packagesfor advanced definitional concepts (like (co-)inductive sets andtypes, well-founded recursion etc.). The distribution also includessome large applications, for example correctness proofs ofcryptographic protocols (HOL/Auth) or communication protocols(HOLCF/IOA).Isabelle/ZF provides another starting point for applications, with aslightly less developed library. Its definitional packages aresimilar to those of Isabelle/HOL. Untyped ZF provides more advancedconstructions for sets than simply-typed HOL.Logics are not hard-wired into Isabelle, but formulated withinIsabelle's meta logic: Isabelle/Pure. There are quite a lot ofsyntactic and deductive tools available in generic Isabelle. Isabelleproof tools provide a high degree of automation.%package HOLSummary: Isabelle Theorem Proving Environment -- Higher-Order LogicGroup: Applications/MathRequires: isabelle%description HOLThis package contains a binary image of the HOL object-logic for Isabelle.%package HOL-RealSummary: Isabelle Theorem Proving Environment -- Higher-Order LogicGroup: Applications/MathRequires: isabelle%description HOL-RealThis package contains a binary image of the HOL object-logic for Isabelle,including support for real numbers.%package ZFSummary: Isabelle Theorem Proving Environment -- Zermelo-Fraenkel set theoryGroup: Applications/MathRequires: isabelle%description ZFThis package contains a binary image of the ZF object-logic for Isabelle.%package pdfdocsSummary: Isabelle Theorem Proving Environment -- PDF documentationGroup: Applications/MathRequires: isabelle%description pdfdocsThis package contains the Isabelle documentation in PDF. Note thatthe 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%postunrm -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 pdfdocsEOFfor F in $(ls -1 doc/*.pdf); do echo "$ISABELLE_HOME/$F" >>$TMP/SPECS/isabelle.specdonecat >>$TMP/SPECS/isabelle.spec <<EOF%files%dir $ISABELLE_HOME%dir $ISABELLE_HOME/doc%dir $ISABELLE_HOME/heaps%dir $ISABELLE_HOME/heaps/${COMPILER}EOFfor F in $(ls -1 | grep -v heaps | grep -v browser_info | grep -v doc); do echo "$ISABELLE_HOME/$F" >>$TMP/SPECS/isabelle.specdonefor F in $(ls -1 doc/* | grep -v pdf); do echo "$ISABELLE_HOME/$F" >>$TMP/SPECS/isabelle.specdone# invoke rpmchown -R root:root "$TMP" || chgrp -R isabelle "$TMP"rpm -bb "$TMP/SPECS/isabelle.spec"mkdir -p "$DISTBASE/rpm"cd /usr/src/packages/RPMS/i386mv "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 upcd /rm -rf "$TMP"