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