# HG changeset patch # User wenzelm # Date 969980720 -7200 # Node ID 5c669ab41d8e2caa4a9ac826115f509b1f1dd27b # Parent 7c2021b7c664727f3906ca31652e5175e55d14c7 got rid of RPM; diff -r 7c2021b7c664 -r 5c669ab41d8e Admin/makerpm --- 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 = ;' \ - -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 < -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 <>$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"