Admin/makerpm
author wenzelm
Wed Sep 20 21:20:01 2000 +0200 (2000-09-20)
changeset 10039 1eb980d64ba3
parent 10014 d41ab495ab14
child 10068 46db6fde4ee3
permissions -rwxr-xr-x
tuned;
     1 #!/bin/bash
     2 #
     3 # $Id$
     4 #
     5 # makerpm -- make Isabelle rpm packages for Linux/x86 from the distribution.
     6 
     7 
     8 ## global settings
     9 
    10 FAKE_BUILD=""
    11 DISTBASE=~/tmp/isadist
    12 ROOT=/usr/share
    13 BIN=/usr/bin
    14 RPMRELEASE=1
    15 
    16 
    17 ## diagnostics
    18 
    19 PRG=$(basename "$0")
    20 
    21 function usage()
    22 {
    23   echo
    24   echo "Usage: $PRG ARCHIVE"
    25   echo
    26   echo "Make Isabelle rpm packages for Linux/x86 from the distribution archives."
    27   echo
    28   exit 1
    29 }
    30 
    31 function fail()
    32 {
    33   echo "$1" >&2
    34   exit 2
    35 }
    36 
    37 
    38 ## process command line
    39 
    40 [ "$#" -gt 1 ] && usage
    41 
    42 ARCHIVE="$1"; shift
    43 
    44 
    45 
    46 ## main
    47 
    48 [ ! -f "$ARCHIVE" ] && fail "Bad archive file $ARCHIVE"
    49 ARCHIVE_BASE=$(basename "$ARCHIVE")
    50 ARCHIVE_DIR=$(cd $(dirname "$ARCHIVE"); echo "$PWD")
    51 ARCHIVE_FULL=$ARCHIVE_DIR/$ARCHIVE_BASE
    52 
    53 ISABELLE_NAME=$(basename "$ARCHIVE_BASE" .tar.gz)
    54 ISABELLE_HOME="$ROOT/$ISABELLE_NAME"
    55 
    56 PDF_ARCHIVE_FULL="$ARCHIVE_DIR/${ISABELLE_NAME}_pdf.tar.gz"
    57 [ ! -f "$PDF_ARCHIVE_FULL" ] && PDF_ARCHIVE_FULL=""
    58 
    59 
    60 # prep
    61 
    62 TMP="/tmp/isabelle-makerpm$$"
    63 for D in "BUILD$ROOT" RPMS/i386 SOURCES SPECS SRPMS; do mkdir -p "$TMP/$D"; done
    64 
    65 cd "$TMP/BUILD$ROOT"
    66 tar -xpzf "$ARCHIVE_FULL"
    67 [ -n "$PDF_ARCHIVE_FULL" ] && tar -xpzf "$PDF_ARCHIVE_FULL"
    68 
    69 
    70 # build
    71 
    72 cd "$TMP/BUILD$ROOT/$ISABELLE_NAME"
    73 ( env BASH_PATH=/bin/bash PERL_PATH=/usr/bin/perl ./configure )
    74 COMPILER=$(./bin/isatool getenv -b ML_IDENTIFIER)
    75 
    76 if [ -n "$FAKE_BUILD" ]; then
    77   mkdir -p heaps/${COMPILER}
    78   touch heaps/${COMPILER}/HOL
    79   touch heaps/${COMPILER}/HOL-Real
    80   touch heaps/${COMPILER}/ZF
    81 else
    82   ./build -b -m HOL-Real HOL
    83   ./build -b ZF
    84   rm -f heaps/${COMPILER}/Pure heaps/${COMPILER}/FOL heaps/${COMPILER}/TLA
    85 fi
    86 
    87 
    88 # rpm spec
    89 
    90 RPMVERSION=$(echo "$ISABELLE_NAME" | perl -w \
    91   -e '$name = <STDIN>;' \
    92   -e 'if ($name =~ m/^Isabelle(\d+)$/) {' \
    93   -e '  $rpmversion = "$1";' \
    94   -e '} elsif ($name =~ m/^Isabelle(\d+)-(\d+)$/) {' \
    95   -e '  $rpmversion = "$1p$2";' \
    96   -e '} elsif ($name =~ m/^Isabelle_(\d+)-(\w+)-(\d+)$/) {' \
    97   -e '  $rpmversion = "$1$2$3";' \
    98   -e '} else {' \
    99   -e '  $rpmversion = "";' \
   100   -e '};' \
   101   -e 'print $rpmversion;')
   102 
   103 [ -z "$RPMVERSION" ] && fail "Unable to derive package version from $ISABELLE_NAME"
   104 
   105 cat >$TMP/SPECS/isabelle.spec <<EOF
   106 Summary:	Isabelle Theorem Proving Environment
   107 Name:		isabelle
   108 Version:	$RPMVERSION
   109 Release:	$RPMRELEASE
   110 Group:		Applications/Math
   111 Copyright:	University of Cambridge Computer Laboratory
   112 Url:		http://www.cl.cam.ac.uk/Research/HVG/Isabelle/
   113 Packager:	Markus Wenzel <wenzelm@in.tum.de>
   114 Prefix:		$ROOT
   115 BuildRoot:	$TMP/BUILD
   116 
   117 %description
   118 
   119 This package contains the full source distribution of Isabelle
   120 together with documentation.  To make it actually run you still need
   121 the ML compiler and any of the precompiled Isabelle object-logics
   122 (e.g. package isabelle-HOL).
   123 
   124 Isabelle is a popular generic theorem proving environment developed at
   125 Cambridge University (Larry Paulson) and TU Munich (Tobias Nipkow).
   126 The system can be viewed from two main perspectives.  On the one hand
   127 it may serve as a generic framework for rapid prototyping of deductive
   128 systems.  On the other hand, major existing logics like Isabelle/HOL
   129 provide a theorem proving environment ready to use for sizable
   130 applications.
   131 
   132 The Isabelle distribution includes a large body of object logics and
   133 other examples (see also the Isabelle theory library at
   134 http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/).  Isabelle/HOL
   135 is a version of classical higher-order logic resembling that of the
   136 HOL System.  Isabelle/HOLCF adds Scott's Logic for Computable
   137 Functions (domain theory) to HOL.  Isabelle/FOL provides basic
   138 classical and intuitionistic first-order logic.  It is polymorphic.
   139 Isabelle/ZF offers a formulation of Zermelo-Fraenkel set theory on top
   140 of FOL.
   141 
   142 Isabelle/HOL is currently the best developed object logic, including
   143 an extensive library of (concrete) mathematics, and various packages
   144 for advanced definitional concepts (like (co-)inductive sets and
   145 types, well-founded recursion etc.).  The distribution also includes
   146 some large applications, for example correctness proofs of
   147 cryptographic protocols (HOL/Auth) or communication protocols
   148 (HOLCF/IOA).
   149 
   150 Isabelle/ZF provides another starting point for applications, with a
   151 slightly less developed library.  Its definitional packages are
   152 similar to those of Isabelle/HOL.  Untyped ZF provides more advanced
   153 constructions for sets than simply-typed HOL.
   154 
   155 Logics are not hard-wired into Isabelle, but formulated within
   156 Isabelle's meta logic: Isabelle/Pure.  There are quite a lot of
   157 syntactic and deductive tools available in generic Isabelle.  Isabelle
   158 proof tools provide a high degree of automation.
   159 
   160 By virtue of the Isabelle/Isar subsystem, interactive proof
   161 development may be performed both via traditional tactic scripts, or
   162 actual human readable (formal) proof texts.  The resulting theory
   163 developments may be presented in high quality as (PDF)LaTeX documents,
   164 accommodating both printed copies and WWW browsing.
   165 
   166 %package	HOL
   167 Summary:	Isabelle Theorem Proving Environment -- Higher-Order Logic
   168 Group:		Applications/Math
   169 Requires:       isabelle
   170 %description HOL
   171 This package contains a binary image of the HOL object-logic for Isabelle.
   172 
   173 %package	HOL-Real
   174 Summary:	Isabelle Theorem Proving Environment -- Higher-Order Logic
   175 Group:		Applications/Math
   176 Requires:       isabelle
   177 %description HOL-Real
   178 This package contains a binary image of the HOL object-logic for Isabelle,
   179 including support for real numbers.
   180 
   181 %package	ZF
   182 Summary:	Isabelle Theorem Proving Environment -- Zermelo-Fraenkel set theory
   183 Group:		Applications/Math
   184 Requires:       isabelle
   185 %description ZF
   186 This package contains a binary image of the ZF object-logic for Isabelle.
   187 
   188 %package	pdfdocs
   189 Summary:	Isabelle Theorem Proving Environment -- PDF documentation
   190 Group:		Applications/Math
   191 Requires:       isabelle
   192 %description pdfdocs
   193 This package contains the Isabelle documentation in PDF.  Note that
   194 the dvi version is already part of the base package.
   195 
   196 %prep
   197 
   198 %build
   199 
   200 %install
   201 
   202 %post
   203 \$RPM_INSTALL_PREFIX/$ISABELLE_NAME/bin/isatool install -p $BIN
   204 
   205 %post HOL
   206 %post HOL-Real
   207 %post ZF
   208 %post pdfdocs
   209 
   210 %postun
   211 rm -f $BIN/Isabelle $BIN/isabelle $BIN/isatool
   212 
   213 %postun HOL
   214 %postun HOL-Real
   215 %postun ZF
   216 %postun pdfdocs
   217 
   218 
   219 %files HOL
   220 $ISABELLE_HOME/heaps/${COMPILER}/HOL
   221 
   222 %files HOL-Real
   223 $ISABELLE_HOME/heaps/${COMPILER}/HOL-Real
   224 
   225 %files ZF
   226 $ISABELLE_HOME/heaps/${COMPILER}/ZF
   227 
   228 %files pdfdocs
   229 EOF
   230 
   231 for F in $(ls -1 doc/*.pdf); do
   232   echo "$ISABELLE_HOME/$F" >>$TMP/SPECS/isabelle.spec
   233 done
   234 
   235 
   236 cat >>$TMP/SPECS/isabelle.spec <<EOF
   237 %files
   238 %dir $ISABELLE_HOME
   239 %dir $ISABELLE_HOME/doc
   240 %dir $ISABELLE_HOME/heaps
   241 %dir $ISABELLE_HOME/heaps/${COMPILER}
   242 EOF
   243 
   244 for F in $(ls -1 | grep -v heaps | grep -v browser_info | grep -v doc); do
   245   echo "$ISABELLE_HOME/$F" >>$TMP/SPECS/isabelle.spec
   246 done
   247 
   248 for F in $(ls -1 doc/* | grep -v pdf); do
   249   echo "$ISABELLE_HOME/$F" >>$TMP/SPECS/isabelle.spec
   250 done
   251 
   252 
   253 # invoke rpm
   254 
   255 chown -R root:root "$TMP" || chgrp -R isabelle "$TMP"
   256 
   257 rpm -bb "$TMP/SPECS/isabelle.spec"
   258 
   259 mkdir -p "$DISTBASE/rpm"
   260 cd /usr/src/packages/RPMS/i386
   261 mv "isabelle-$RPMVERSION-${RPMRELEASE}.i386.rpm" "$DISTBASE/rpm/isabelle.rpm"
   262 mv "isabelle-HOL-$RPMVERSION-${RPMRELEASE}.i386.rpm" "$DISTBASE/rpm/isabelle-HOL.i386.rpm"
   263 mv "isabelle-HOL-Real-$RPMVERSION-${RPMRELEASE}.i386.rpm" "$DISTBASE/rpm/isabelle-HOL-Real.i386.rpm"
   264 mv "isabelle-ZF-$RPMVERSION-${RPMRELEASE}.i386.rpm" "$DISTBASE/rpm/isabelle-ZF.i386.rpm"
   265 mv "isabelle-pdfdocs-$RPMVERSION-${RPMRELEASE}.i386.rpm" "$DISTBASE/rpm/isabelle-pdfdocs.rpm"
   266 
   267 # clean up
   268 cd /
   269 rm -rf "$TMP"