Admin/makerpm
author wenzelm
Mon, 13 Mar 2000 13:21:39 +0100
changeset 8434 5e4bba59bfaa
parent 8317 a959dfeeacc6
child 8853 079f607dc3dd
permissions -rwxr-xr-x
use HOLogic.Not; export indexify_names;
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
8317
wenzelm
parents: 8046
diff changeset
    14
RPMRELEASE=2
6485
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
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    17
## diagnostics
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    18
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    19
PRG=$(basename $0)
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    20
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    21
function usage()
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    22
{
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    23
  echo
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    24
  echo "Usage: $PRG ARCHIVE"
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    25
  echo
7488
c49d17fac066 isabelle-pdfdocs;
wenzelm
parents: 7337
diff changeset
    26
  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
    27
  echo
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    28
  exit 1
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
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    31
function fail()
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    32
{
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    33
  echo "$1" >&2
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    34
  exit 2
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
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    38
## process command line
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    39
7488
c49d17fac066 isabelle-pdfdocs;
wenzelm
parents: 7337
diff changeset
    40
[ $# -gt 1 ] && usage
6485
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    41
7488
c49d17fac066 isabelle-pdfdocs;
wenzelm
parents: 7337
diff changeset
    42
ARCHIVE="$1"; shift
c49d17fac066 isabelle-pdfdocs;
wenzelm
parents: 7337
diff changeset
    43
6485
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
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    46
## main
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    47
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    48
[ ! -f "$ARCHIVE" ] && fail "Bad archive file $ARCHIVE"
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    49
ARCHIVE_BASE=$(basename "$ARCHIVE")
7488
c49d17fac066 isabelle-pdfdocs;
wenzelm
parents: 7337
diff changeset
    50
ARCHIVE_DIR=$(cd $(dirname "$ARCHIVE"); echo $PWD)
c49d17fac066 isabelle-pdfdocs;
wenzelm
parents: 7337
diff changeset
    51
ARCHIVE_FULL=$ARCHIVE_DIR/$ARCHIVE_BASE
6485
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    52
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    53
ISABELLE_NAME=$(basename "$ARCHIVE_BASE" .tar.gz)
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    54
ISABELLE_HOME="$ROOT/$ISABELLE_NAME"
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    55
7488
c49d17fac066 isabelle-pdfdocs;
wenzelm
parents: 7337
diff changeset
    56
PDF_ARCHIVE_FULL="$ARCHIVE_DIR/${ISABELLE_NAME}_pdf.tar.gz"
c49d17fac066 isabelle-pdfdocs;
wenzelm
parents: 7337
diff changeset
    57
[ ! -f "$PDF_ARCHIVE_FULL" ] && PDF_ARCHIVE_FULL=""
c49d17fac066 isabelle-pdfdocs;
wenzelm
parents: 7337
diff changeset
    58
6485
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
# prep
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    61
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    62
TMP="/tmp/isabelle-makerpm$$"
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    63
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
    64
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    65
cd "$TMP/BUILD$ROOT"
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    66
tar -xpzf "$ARCHIVE_FULL"
7488
c49d17fac066 isabelle-pdfdocs;
wenzelm
parents: 7337
diff changeset
    67
[ -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
    68
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    69
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    70
# build
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
cd "$TMP/BUILD$ROOT/$ISABELLE_NAME"
7488
c49d17fac066 isabelle-pdfdocs;
wenzelm
parents: 7337
diff changeset
    73
( env BASH_PATH=/bin/bash PERL_PATH=/usr/bin/perl ./configure )
7312
523fb2832b30 added HOL-Real;
wenzelm
parents: 6608
diff changeset
    74
./build -bi $LOGICS
6485
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    75
COMPILER=$(./bin/isatool getenv -b ML_IDENTIFIER)
7314
wenzelm
parents: 7312
diff changeset
    76
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
    77
8046
91587887bcbf accommodate current version of rpm;
wenzelm
parents: 7992
diff changeset
    78
# fake build
91587887bcbf accommodate current version of rpm;
wenzelm
parents: 7992
diff changeset
    79
#mkdir -p heaps/${COMPILER}
91587887bcbf accommodate current version of rpm;
wenzelm
parents: 7992
diff changeset
    80
#touch heaps/${COMPILER}/HOL
91587887bcbf accommodate current version of rpm;
wenzelm
parents: 7992
diff changeset
    81
#touch heaps/${COMPILER}/HOL-Real
91587887bcbf accommodate current version of rpm;
wenzelm
parents: 7992
diff changeset
    82
#touch heaps/${COMPILER}/ZF
91587887bcbf accommodate current version of rpm;
wenzelm
parents: 7992
diff changeset
    83
6485
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    84
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    85
# rpm spec
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    86
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    87
RPMVERSION=$(echo "$ISABELLE_NAME" | perl -w \
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    88
  -e '$name = <STDIN>;' \
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    89
  -e 'if ($name =~ m/^Isabelle(\d+)$/) {' \
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    90
  -e '  $rpmversion = "$1";' \
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    91
  -e '} elsif ($name =~ m/^Isabelle(\d+)-(\d+)$/) {' \
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    92
  -e '  $rpmversion = "$1p$2";' \
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    93
  -e '} elsif ($name =~ m/^Isabelle_(\d+)-(\w+)-(\d+)$/) {' \
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    94
  -e '  $rpmversion = "$1$2$3";' \
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    95
  -e '} else {' \
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    96
  -e '  $rpmversion = "";' \
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    97
  -e '};' \
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    98
  -e 'print $rpmversion;')
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
    99
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   100
[ -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
   101
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   102
cat >$TMP/SPECS/isabelle.spec <<EOF
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   103
Summary:	Isabelle Theorem Proving Environment
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   104
Name:		isabelle
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   105
Version:	$RPMVERSION
7992
6f49fe89bfe1 RPMRELEASE;
wenzelm
parents: 7488
diff changeset
   106
Release:	$RPMRELEASE
6485
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   107
Group:		Applications/Math
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   108
Copyright:	University of Cambridge Computer Laboratory
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   109
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
   110
Packager:	Markus Wenzel <wenzelm@in.tum.de>
7312
523fb2832b30 added HOL-Real;
wenzelm
parents: 6608
diff changeset
   111
Prefix:		$ROOT
6485
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   112
BuildRoot:	$TMP/BUILD
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
%description
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   115
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   116
This package contains the full source distribution of Isabelle
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   117
together with documentation.  To make it actually run you still need
8317
wenzelm
parents: 8046
diff changeset
   118
the ML compiler and any of the precompiled Isabelle object-logics
wenzelm
parents: 8046
diff changeset
   119
(e.g. package isabelle-HOL).
6485
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   120
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   121
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   122
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
   123
Cambridge University (Larry Paulson) and TU Munich (Tobias Nipkow).
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   124
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
   125
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
   126
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
   127
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
   128
applications.
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   129
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   130
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
   131
other examples (see also the Isabelle theory library at
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   132
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
   133
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
   134
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
   135
Functions (domain theory) to HOL.  Isabelle/FOL provides basic
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   136
classical and intuitionistic first-order logic.  It is polymorphic.
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   137
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
   138
of FOL.
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   139
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   140
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
   141
an extensive library of (concrete) mathematics, and various packages
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   142
for advanced definitional concepts (like (co-)inductive sets and
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   143
types, well-founded recursion etc.).  The distribution also includes
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   144
some large applications, for example correctness proofs of
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   145
cryptographic protocols (HOL/Auth) or communication protocols
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   146
(HOLCF/IOA).
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   147
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   148
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
   149
slightly less developed library.  Its definitional packages are
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   150
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
   151
constructions for sets than simply-typed HOL.
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   152
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   153
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
   154
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
   155
syntactic and deductive tools available in generic Isabelle.  Isabelle
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   156
proof tools provide a high degree of automation.
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   157
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   158
%package	HOL
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   159
Summary:	Isabelle Theorem Proving Environment -- Higher-Order Logic
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   160
Group:		Applications/Math
6567
8338dd394144 fixed reqs?
wenzelm
parents: 6562
diff changeset
   161
Requires:       isabelle
6485
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   162
%description HOL
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   163
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
   164
7312
523fb2832b30 added HOL-Real;
wenzelm
parents: 6608
diff changeset
   165
%package	HOL-Real
523fb2832b30 added HOL-Real;
wenzelm
parents: 6608
diff changeset
   166
Summary:	Isabelle Theorem Proving Environment -- Higher-Order Logic
523fb2832b30 added HOL-Real;
wenzelm
parents: 6608
diff changeset
   167
Group:		Applications/Math
523fb2832b30 added HOL-Real;
wenzelm
parents: 6608
diff changeset
   168
Requires:       isabelle
523fb2832b30 added HOL-Real;
wenzelm
parents: 6608
diff changeset
   169
%description HOL-Real
523fb2832b30 added HOL-Real;
wenzelm
parents: 6608
diff changeset
   170
This package contains a binary image of the HOL object-logic for Isabelle,
523fb2832b30 added HOL-Real;
wenzelm
parents: 6608
diff changeset
   171
including support for real numbers.
523fb2832b30 added HOL-Real;
wenzelm
parents: 6608
diff changeset
   172
6485
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   173
%package	ZF
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   174
Summary:	Isabelle Theorem Proving Environment -- Zermelo-Fraenkel set theory
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   175
Group:		Applications/Math
6567
8338dd394144 fixed reqs?
wenzelm
parents: 6562
diff changeset
   176
Requires:       isabelle
6485
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   177
%description ZF
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   178
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
   179
7488
c49d17fac066 isabelle-pdfdocs;
wenzelm
parents: 7337
diff changeset
   180
%package	pdfdocs
c49d17fac066 isabelle-pdfdocs;
wenzelm
parents: 7337
diff changeset
   181
Summary:	Isabelle Theorem Proving Environment -- PDF documentation
c49d17fac066 isabelle-pdfdocs;
wenzelm
parents: 7337
diff changeset
   182
Group:		Applications/Math
c49d17fac066 isabelle-pdfdocs;
wenzelm
parents: 7337
diff changeset
   183
Requires:       isabelle
c49d17fac066 isabelle-pdfdocs;
wenzelm
parents: 7337
diff changeset
   184
%description pdfdocs
c49d17fac066 isabelle-pdfdocs;
wenzelm
parents: 7337
diff changeset
   185
This package contains the Isabelle documentation in PDF.  Note that
c49d17fac066 isabelle-pdfdocs;
wenzelm
parents: 7337
diff changeset
   186
the dvi version is already part of the base package.
c49d17fac066 isabelle-pdfdocs;
wenzelm
parents: 7337
diff changeset
   187
7312
523fb2832b30 added HOL-Real;
wenzelm
parents: 6608
diff changeset
   188
6485
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   189
%prep
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   190
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   191
%build
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   192
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   193
%install
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   194
7312
523fb2832b30 added HOL-Real;
wenzelm
parents: 6608
diff changeset
   195
%post
523fb2832b30 added HOL-Real;
wenzelm
parents: 6608
diff changeset
   196
\$RPM_INSTALL_PREFIX/$ISABELLE_NAME/bin/isatool install -p $BIN
523fb2832b30 added HOL-Real;
wenzelm
parents: 6608
diff changeset
   197
523fb2832b30 added HOL-Real;
wenzelm
parents: 6608
diff changeset
   198
%post HOL
523fb2832b30 added HOL-Real;
wenzelm
parents: 6608
diff changeset
   199
%post HOL-Real
523fb2832b30 added HOL-Real;
wenzelm
parents: 6608
diff changeset
   200
%post ZF
7488
c49d17fac066 isabelle-pdfdocs;
wenzelm
parents: 7337
diff changeset
   201
%post pdfdocs
7312
523fb2832b30 added HOL-Real;
wenzelm
parents: 6608
diff changeset
   202
523fb2832b30 added HOL-Real;
wenzelm
parents: 6608
diff changeset
   203
%postun
523fb2832b30 added HOL-Real;
wenzelm
parents: 6608
diff changeset
   204
rm -f $BIN/Isabelle $BIN/isabelle $BIN/isatool
523fb2832b30 added HOL-Real;
wenzelm
parents: 6608
diff changeset
   205
523fb2832b30 added HOL-Real;
wenzelm
parents: 6608
diff changeset
   206
%postun HOL
523fb2832b30 added HOL-Real;
wenzelm
parents: 6608
diff changeset
   207
%postun HOL-Real
523fb2832b30 added HOL-Real;
wenzelm
parents: 6608
diff changeset
   208
%postun ZF
7488
c49d17fac066 isabelle-pdfdocs;
wenzelm
parents: 7337
diff changeset
   209
%postun pdfdocs
7312
523fb2832b30 added HOL-Real;
wenzelm
parents: 6608
diff changeset
   210
523fb2832b30 added HOL-Real;
wenzelm
parents: 6608
diff changeset
   211
6485
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   212
%files HOL
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   213
$ISABELLE_HOME/heaps/${COMPILER}/HOL
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   214
7312
523fb2832b30 added HOL-Real;
wenzelm
parents: 6608
diff changeset
   215
%files HOL-Real
523fb2832b30 added HOL-Real;
wenzelm
parents: 6608
diff changeset
   216
$ISABELLE_HOME/heaps/${COMPILER}/HOL-Real
523fb2832b30 added HOL-Real;
wenzelm
parents: 6608
diff changeset
   217
6485
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   218
%files ZF
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   219
$ISABELLE_HOME/heaps/${COMPILER}/ZF
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   220
7488
c49d17fac066 isabelle-pdfdocs;
wenzelm
parents: 7337
diff changeset
   221
%files pdfdocs
c49d17fac066 isabelle-pdfdocs;
wenzelm
parents: 7337
diff changeset
   222
EOF
c49d17fac066 isabelle-pdfdocs;
wenzelm
parents: 7337
diff changeset
   223
c49d17fac066 isabelle-pdfdocs;
wenzelm
parents: 7337
diff changeset
   224
for F in $(ls -1 doc/*.pdf); do
c49d17fac066 isabelle-pdfdocs;
wenzelm
parents: 7337
diff changeset
   225
  echo "$ISABELLE_HOME/$F" >>$TMP/SPECS/isabelle.spec
c49d17fac066 isabelle-pdfdocs;
wenzelm
parents: 7337
diff changeset
   226
done
c49d17fac066 isabelle-pdfdocs;
wenzelm
parents: 7337
diff changeset
   227
c49d17fac066 isabelle-pdfdocs;
wenzelm
parents: 7337
diff changeset
   228
c49d17fac066 isabelle-pdfdocs;
wenzelm
parents: 7337
diff changeset
   229
cat >>$TMP/SPECS/isabelle.spec <<EOF
6485
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   230
%files
7337
wenzelm
parents: 7314
diff changeset
   231
%dir $ISABELLE_HOME
7488
c49d17fac066 isabelle-pdfdocs;
wenzelm
parents: 7337
diff changeset
   232
%dir $ISABELLE_HOME/doc
7337
wenzelm
parents: 7314
diff changeset
   233
%dir $ISABELLE_HOME/heaps
wenzelm
parents: 7314
diff changeset
   234
%dir $ISABELLE_HOME/heaps/${COMPILER}
6485
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   235
EOF
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   236
7488
c49d17fac066 isabelle-pdfdocs;
wenzelm
parents: 7337
diff changeset
   237
for F in $(ls -1 | grep -v heaps | grep -v browser_info | grep -v doc); do
c49d17fac066 isabelle-pdfdocs;
wenzelm
parents: 7337
diff changeset
   238
  echo "$ISABELLE_HOME/$F" >>$TMP/SPECS/isabelle.spec
c49d17fac066 isabelle-pdfdocs;
wenzelm
parents: 7337
diff changeset
   239
done
c49d17fac066 isabelle-pdfdocs;
wenzelm
parents: 7337
diff changeset
   240
c49d17fac066 isabelle-pdfdocs;
wenzelm
parents: 7337
diff changeset
   241
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
   242
  echo "$ISABELLE_HOME/$F" >>$TMP/SPECS/isabelle.spec
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   243
done
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   244
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
# invoke rpm
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   247
6561
793b33191ce3 try chown root:root;
wenzelm
parents: 6499
diff changeset
   248
chown -R root:root "$TMP" || chgrp -R isabelle "$TMP"
6495
d3b8440e1d47 chgrp isabelle;
wenzelm
parents: 6485
diff changeset
   249
8046
91587887bcbf accommodate current version of rpm;
wenzelm
parents: 7992
diff changeset
   250
rpm -bb "$TMP/SPECS/isabelle.spec"
6485
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   251
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   252
mkdir -p "$DISTBASE/rpm"
8046
91587887bcbf accommodate current version of rpm;
wenzelm
parents: 7992
diff changeset
   253
cd /usr/src/packages/RPMS/i386
91587887bcbf accommodate current version of rpm;
wenzelm
parents: 7992
diff changeset
   254
mv "isabelle-$RPMVERSION-${RPMRELEASE}.i386.rpm" "$DISTBASE/rpm/isabelle.rpm"
91587887bcbf accommodate current version of rpm;
wenzelm
parents: 7992
diff changeset
   255
mv "isabelle-HOL-$RPMVERSION-${RPMRELEASE}.i386.rpm" "$DISTBASE/rpm/isabelle-HOL.i386.rpm"
91587887bcbf accommodate current version of rpm;
wenzelm
parents: 7992
diff changeset
   256
mv "isabelle-HOL-Real-$RPMVERSION-${RPMRELEASE}.i386.rpm" "$DISTBASE/rpm/isabelle-HOL-Real.i386.rpm"
91587887bcbf accommodate current version of rpm;
wenzelm
parents: 7992
diff changeset
   257
mv "isabelle-ZF-$RPMVERSION-${RPMRELEASE}.i386.rpm" "$DISTBASE/rpm/isabelle-ZF.i386.rpm"
91587887bcbf accommodate current version of rpm;
wenzelm
parents: 7992
diff changeset
   258
mv "isabelle-pdfdocs-$RPMVERSION-${RPMRELEASE}.i386.rpm" "$DISTBASE/rpm/isabelle-pdfdocs.rpm"
6485
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   259
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   260
# clean up
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   261
cd /
0d334465f29a make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff changeset
   262
rm -rf "$TMP"