--- a/Admin/makerpm Tue Sep 26 17:05:01 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,272 +0,0 @@
-#!/bin/bash
-#
-# $Id$
-#
-# makerpm -- make Isabelle rpm packages for Linux/x86 from the distribution.
-
-
-## global settings
-
-FAKE_BUILD=""
-DISTBASE=~/tmp/isadist
-ROOT=/usr/share
-BIN=/usr/bin
-RPMRELEASE=1
-
-
-## 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"
-
-rm -f Isabelle
-ln -s "$ISABELLE_NAME" Isabelle
-
-
-# build
-
-cd "$TMP/BUILD$ROOT/$ISABELLE_NAME"
-( env BASH_PATH=/bin/bash PERL_PATH=/usr/bin/perl ./configure )
-COMPILER=$(./bin/isatool getenv -b ML_IDENTIFIER)
-
-if [ -n "$FAKE_BUILD" ]; then
- mkdir -p heaps/${COMPILER}
- touch heaps/${COMPILER}/HOL
- touch heaps/${COMPILER}/HOL-Real
- touch heaps/${COMPILER}/ZF
-else
- ./build -b -m HOL-Real HOL
- ./build -b ZF
- rm -f heaps/${COMPILER}/Pure heaps/${COMPILER}/FOL heaps/${COMPILER}/TLA
-fi
-
-
-# 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.
-
-By virtue of the Isabelle/Isar subsystem, interactive proof
-development may be performed both via traditional tactic scripts, or
-actual human readable (formal) proof texts. The resulting theory
-developments may be presented in high quality as (PDF)LaTeX documents,
-accommodating both printed copies and WWW browsing.
-
-%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
-$ROOT/Isabelle
-%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"
-
-cd /usr/src/packages/RPMS/i386
-mv "isabelle-$RPMVERSION-${RPMRELEASE}.i386.rpm" "$DISTBASE/isabelle.rpm"
-mv "isabelle-HOL-$RPMVERSION-${RPMRELEASE}.i386.rpm" "$DISTBASE/isabelle-HOL.i386.rpm"
-mv "isabelle-HOL-Real-$RPMVERSION-${RPMRELEASE}.i386.rpm" "$DISTBASE/isabelle-HOL-Real.i386.rpm"
-mv "isabelle-ZF-$RPMVERSION-${RPMRELEASE}.i386.rpm" "$DISTBASE/isabelle-ZF.i386.rpm"
-mv "isabelle-pdfdocs-$RPMVERSION-${RPMRELEASE}.i386.rpm" "$DISTBASE/isabelle-pdfdocs.rpm"
-
-# clean up
-cd /
-rm -rf "$TMP"