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