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