diff -r 3f098b0ec683 -r 0d334465f29a Admin/makerpm
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/makerpm	Thu Apr 22 15:03:50 1999 +0200
@@ -0,0 +1,197 @@
+#!/bin/bash
+#
+# $Id$
+#
+# makerpm -- make Isabelle rpm packages for Linux/x86 from the distribution.
+
+
+## global settings
+
+LOGICS="HOL ZF"
+DISTBASE=~/tmp/isadist
+ROOT=/usr/local
+BIN=/usr/local/bin
+
+
+## diagnostics
+
+PRG=$(basename $0)
+
+function usage()
+{
+  echo
+  echo "Usage: $PRG ARCHIVE"
+  echo
+  echo "Make Isabelle rpm packages for Linux/x86 from distribution ARCHIVE."
+  echo
+  exit 1
+}
+
+function fail()
+{
+  echo "$1" >&2
+  exit 2
+}
+
+
+## process command line
+
+[ $# -ne 1 ] && usage
+
+ARCHIVE="$1"
+shift
+
+
+## main
+
+[ ! -f "$ARCHIVE" ] && fail "Bad archive file $ARCHIVE"
+ARCHIVE_BASE=$(basename "$ARCHIVE")
+ARCHIVE_FULL=$(cd $(dirname "$ARCHIVE"); echo $PWD)/$ARCHIVE_BASE
+
+ISABELLE_NAME=$(basename "$ARCHIVE_BASE" .tar.gz)
+ISABELLE_HOME="$ROOT/$ISABELLE_NAME"
+
+
+# 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"
+
+
+# build
+
+cd "$TMP/BUILD$ROOT/$ISABELLE_NAME"
+./configure
+./build -b $LOGICS
+./bin/isatool install -d "$ISABELLE_HOME" -p "$TMP/BUILD$BIN"
+COMPILER=$(./bin/isatool getenv -b ML_IDENTIFIER)
+
+
+# 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:	1
+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>
+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 SML/NJ 110 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:       %{name} = %{version}
+%description HOL
+This package contains a binary image of the HOL object-logic for Isabelle.
+
+%package	ZF
+Summary:	Isabelle Theorem Proving Environment -- Zermelo-Fraenkel set theory
+Group:		Applications/Math
+Requires:       %{name} = %{version}
+%description ZF
+This package contains a binary image of the ZF object-logic for Isabelle.
+
+%prep
+
+%build
+
+%install
+
+%files HOL
+$ISABELLE_HOME/heaps/${COMPILER}/HOL
+
+%files ZF
+$ISABELLE_HOME/heaps/${COMPILER}/ZF
+
+%files
+$BIN/Isabelle
+$BIN/isabelle
+$BIN/isatool
+%dir $ISABELLE_HOME
+EOF
+
+for F in $(ls -1 | grep -v heaps | grep -v browser_info)
+do
+  echo "$ISABELLE_HOME/$F" >>$TMP/SPECS/isabelle.spec
+done
+
+
+# invoke rpm
+
+echo "topdir: $TMP" >"$TMP/rpmrc"
+rpm --rcfile "$TMP/rpmrc" -bb "$TMP/SPECS/isabelle.spec"
+
+mkdir -p "$DISTBASE/rpm"
+cd "$TMP/RPMS/i386"
+cp "isabelle-$RPMVERSION-1.i386.rpm" "$DISTBASE/rpm/isabelle.rpm"
+cp "isabelle-HOL-$RPMVERSION-1.i386.rpm" "$DISTBASE/rpm/isabelle-HOL.i386.rpm"
+cp "isabelle-ZF-$RPMVERSION-1.i386.rpm" "$DISTBASE/rpm/isabelle-ZF.i386.rpm"
+
+# clean up
+cd /
+rm -rf "$TMP"