Admin/makerpm
author wenzelm
Tue, 24 Aug 1999 23:28:02 +0200
changeset 7337 3f8eeb0b6d75
parent 7314 d3968533692c
child 7488 c49d17fac066
permissions -rwxr-xr-x
%dir;
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
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    25
  echo "Make Isabelle rpm packages for Linux/x86 from distribution ARCHIVE."
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
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    39
[ $# -ne 1 ] && usage
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    40
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    41
ARCHIVE="$1"
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    42
shift
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")
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    49
ARCHIVE_FULL=$(cd $(dirname "$ARCHIVE"); echo $PWD)/$ARCHIVE_BASE
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    50
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    51
ISABELLE_NAME=$(basename "$ARCHIVE_BASE" .tar.gz)
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    52
ISABELLE_HOME="$ROOT/$ISABELLE_NAME"
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    53
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    54
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    55
# prep
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    56
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    57
TMP="/tmp/isabelle-makerpm$$"
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    58
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
    59
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    60
cd "$TMP/BUILD$ROOT"
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    61
tar -xpzf "$ARCHIVE_FULL"
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    62
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
# build
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    65
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    66
cd "$TMP/BUILD$ROOT/$ISABELLE_NAME"
7312
523fb2832b30 added HOL-Real;
wenzelm
parents: 6608
diff changeset
    67
( PATH=/bin:$PATH; BASH_PATH=/bin/bash PERL_PATH=/usr/bin/perl ./configure )
523fb2832b30 added HOL-Real;
wenzelm
parents: 6608
diff changeset
    68
./build -bi $LOGICS
6485
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    69
COMPILER=$(./bin/isatool getenv -b ML_IDENTIFIER)
7314
wenzelm
parents: 7312
diff changeset
    70
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
    71
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    72
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    73
# rpm spec
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    74
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    75
RPMVERSION=$(echo "$ISABELLE_NAME" | perl -w \
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    76
  -e '$name = <STDIN>;' \
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    77
  -e 'if ($name =~ m/^Isabelle(\d+)$/) {' \
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    78
  -e '  $rpmversion = "$1";' \
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    79
  -e '} elsif ($name =~ m/^Isabelle(\d+)-(\d+)$/) {' \
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    80
  -e '  $rpmversion = "$1p$2";' \
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    81
  -e '} elsif ($name =~ m/^Isabelle_(\d+)-(\w+)-(\d+)$/) {' \
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    82
  -e '  $rpmversion = "$1$2$3";' \
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    83
  -e '} else {' \
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    84
  -e '  $rpmversion = "";' \
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    85
  -e '};' \
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    86
  -e 'print $rpmversion;')
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    87
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    88
[ -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
    89
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    90
cat >$TMP/SPECS/isabelle.spec <<EOF
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    91
Summary:	Isabelle Theorem Proving Environment
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    92
Name:		isabelle
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    93
Version:	$RPMVERSION
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    94
Release:	1
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    95
Group:		Applications/Math
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    96
Copyright:	University of Cambridge Computer Laboratory
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    97
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
    98
Packager:	Markus Wenzel <wenzelm@in.tum.de>
7312
523fb2832b30 added HOL-Real;
wenzelm
parents: 6608
diff changeset
    99
Prefix:		$ROOT
6485
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   100
BuildRoot:	$TMP/BUILD
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   101
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   102
%description
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   103
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   104
This package contains the full source distribution of Isabelle
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   105
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
   106
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
   107
object-logics (e.g. package isabelle-HOL).
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
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   110
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
   111
Cambridge University (Larry Paulson) and TU Munich (Tobias Nipkow).
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   112
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
   113
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
   114
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
   115
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
   116
applications.
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   117
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   118
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
   119
other examples (see also the Isabelle theory library at
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   120
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
   121
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
   122
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
   123
Functions (domain theory) to HOL.  Isabelle/FOL provides basic
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   124
classical and intuitionistic first-order logic.  It is polymorphic.
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   125
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
   126
of FOL.
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   127
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   128
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
   129
an extensive library of (concrete) mathematics, and various packages
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   130
for advanced definitional concepts (like (co-)inductive sets and
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   131
types, well-founded recursion etc.).  The distribution also includes
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   132
some large applications, for example correctness proofs of
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   133
cryptographic protocols (HOL/Auth) or communication protocols
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   134
(HOLCF/IOA).
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   135
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   136
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
   137
slightly less developed library.  Its definitional packages are
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   138
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
   139
constructions for sets than simply-typed HOL.
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
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
   142
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
   143
syntactic and deductive tools available in generic Isabelle.  Isabelle
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   144
proof tools provide a high degree of automation.
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   145
7312
523fb2832b30 added HOL-Real;
wenzelm
parents: 6608
diff changeset
   146
6485
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   147
%package	HOL
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   148
Summary:	Isabelle Theorem Proving Environment -- Higher-Order Logic
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   149
Group:		Applications/Math
6567
8338dd394144 fixed reqs?
wenzelm
parents: 6562
diff changeset
   150
Requires:       isabelle
6485
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   151
%description HOL
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   152
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
   153
7312
523fb2832b30 added HOL-Real;
wenzelm
parents: 6608
diff changeset
   154
523fb2832b30 added HOL-Real;
wenzelm
parents: 6608
diff changeset
   155
%package	HOL-Real
523fb2832b30 added HOL-Real;
wenzelm
parents: 6608
diff changeset
   156
Summary:	Isabelle Theorem Proving Environment -- Higher-Order Logic
523fb2832b30 added HOL-Real;
wenzelm
parents: 6608
diff changeset
   157
Group:		Applications/Math
523fb2832b30 added HOL-Real;
wenzelm
parents: 6608
diff changeset
   158
Requires:       isabelle
523fb2832b30 added HOL-Real;
wenzelm
parents: 6608
diff changeset
   159
%description HOL-Real
523fb2832b30 added HOL-Real;
wenzelm
parents: 6608
diff changeset
   160
This package contains a binary image of the HOL object-logic for Isabelle,
523fb2832b30 added HOL-Real;
wenzelm
parents: 6608
diff changeset
   161
including support for real numbers.
523fb2832b30 added HOL-Real;
wenzelm
parents: 6608
diff changeset
   162
523fb2832b30 added HOL-Real;
wenzelm
parents: 6608
diff changeset
   163
6485
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   164
%package	ZF
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   165
Summary:	Isabelle Theorem Proving Environment -- Zermelo-Fraenkel set theory
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   166
Group:		Applications/Math
6567
8338dd394144 fixed reqs?
wenzelm
parents: 6562
diff changeset
   167
Requires:       isabelle
6485
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   168
%description ZF
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   169
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
   170
7312
523fb2832b30 added HOL-Real;
wenzelm
parents: 6608
diff changeset
   171
6485
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   172
%prep
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   173
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   174
%build
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   175
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   176
%install
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   177
7312
523fb2832b30 added HOL-Real;
wenzelm
parents: 6608
diff changeset
   178
%post
523fb2832b30 added HOL-Real;
wenzelm
parents: 6608
diff changeset
   179
\$RPM_INSTALL_PREFIX/$ISABELLE_NAME/bin/isatool install -p $BIN
523fb2832b30 added HOL-Real;
wenzelm
parents: 6608
diff changeset
   180
523fb2832b30 added HOL-Real;
wenzelm
parents: 6608
diff changeset
   181
%post HOL
523fb2832b30 added HOL-Real;
wenzelm
parents: 6608
diff changeset
   182
%post HOL-Real
523fb2832b30 added HOL-Real;
wenzelm
parents: 6608
diff changeset
   183
%post ZF
523fb2832b30 added HOL-Real;
wenzelm
parents: 6608
diff changeset
   184
523fb2832b30 added HOL-Real;
wenzelm
parents: 6608
diff changeset
   185
%postun
523fb2832b30 added HOL-Real;
wenzelm
parents: 6608
diff changeset
   186
rm -f $BIN/Isabelle $BIN/isabelle $BIN/isatool
523fb2832b30 added HOL-Real;
wenzelm
parents: 6608
diff changeset
   187
523fb2832b30 added HOL-Real;
wenzelm
parents: 6608
diff changeset
   188
%postun HOL
523fb2832b30 added HOL-Real;
wenzelm
parents: 6608
diff changeset
   189
%postun HOL-Real
523fb2832b30 added HOL-Real;
wenzelm
parents: 6608
diff changeset
   190
%postun ZF
523fb2832b30 added HOL-Real;
wenzelm
parents: 6608
diff changeset
   191
523fb2832b30 added HOL-Real;
wenzelm
parents: 6608
diff changeset
   192
6485
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   193
%files HOL
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   194
$ISABELLE_HOME/heaps/${COMPILER}/HOL
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   195
7312
523fb2832b30 added HOL-Real;
wenzelm
parents: 6608
diff changeset
   196
%files HOL-Real
523fb2832b30 added HOL-Real;
wenzelm
parents: 6608
diff changeset
   197
$ISABELLE_HOME/heaps/${COMPILER}/HOL-Real
523fb2832b30 added HOL-Real;
wenzelm
parents: 6608
diff changeset
   198
6485
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   199
%files ZF
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   200
$ISABELLE_HOME/heaps/${COMPILER}/ZF
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   201
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   202
%files
7337
wenzelm
parents: 7314
diff changeset
   203
%dir $ISABELLE_HOME
wenzelm
parents: 7314
diff changeset
   204
%dir $ISABELLE_HOME/heaps
wenzelm
parents: 7314
diff changeset
   205
%dir $ISABELLE_HOME/heaps/${COMPILER}
6485
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   206
EOF
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   207
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   208
for F in $(ls -1 | grep -v heaps | grep -v browser_info)
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   209
do
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   210
  echo "$ISABELLE_HOME/$F" >>$TMP/SPECS/isabelle.spec
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   211
done
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   212
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   213
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   214
# invoke rpm
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   215
6561
793b33191ce3 try chown root:root;
wenzelm
parents: 6499
diff changeset
   216
chown -R root:root "$TMP" || chgrp -R isabelle "$TMP"
6495
d3b8440e1d47 chgrp isabelle;
wenzelm
parents: 6485
diff changeset
   217
6485
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   218
echo "topdir: $TMP" >"$TMP/rpmrc"
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   219
rpm --rcfile "$TMP/rpmrc" -bb "$TMP/SPECS/isabelle.spec"
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   220
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   221
mkdir -p "$DISTBASE/rpm"
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   222
cd "$TMP/RPMS/i386"
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   223
cp "isabelle-$RPMVERSION-1.i386.rpm" "$DISTBASE/rpm/isabelle.rpm"
7312
523fb2832b30 added HOL-Real;
wenzelm
parents: 6608
diff changeset
   224
cp "isabelle-HOL-$RPMVERSION-1.i386.rpm" "$DISTBASE/rpm/isabelle-HOL.i386.rpm"
7314
wenzelm
parents: 7312
diff changeset
   225
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
   226
cp "isabelle-ZF-$RPMVERSION-1.i386.rpm" "$DISTBASE/rpm/isabelle-ZF.i386.rpm"
6485
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   227
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   228
# clean up
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   229
cd /
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   230
rm -rf "$TMP"