author  wenzelm 
Wed, 01 Dec 1999 22:38:35 +0100  
changeset 8046  91587887bcbf 
parent 7992  6f49fe89bfe1 
child 8317  a959dfeeacc6 
permissions  rwxrxrx 
7314  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  12 
ROOT=/usr/share 
13 
BIN=/usr/bin 

8046  14 
RPMRELEASE=1 
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  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  40 
[ $# gt 1 ] && usage 
6485
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

41 

7488  42 
ARCHIVE="$1"; shift 
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  50 
ARCHIVE_DIR=$(cd $(dirname "$ARCHIVE"); echo $PWD) 
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  56 
PDF_ARCHIVE_FULL="$ARCHIVE_DIR/${ISABELLE_NAME}_pdf.tar.gz" 
57 
[ ! f "$PDF_ARCHIVE_FULL" ] && PDF_ARCHIVE_FULL="" 

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/isabellemakerpm$$" 
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  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  73 
( env BASH_PATH=/bin/bash PERL_PATH=/usr/bin/perl ./configure ) 
7312  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  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  78 
# fake build 
79 
#mkdir p heaps/${COMPILER} 

80 
#touch heaps/${COMPILER}/HOL 

81 
#touch heaps/${COMPILER}/HOLReal 

82 
#touch heaps/${COMPILER}/ZF 

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  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  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 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

118 
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

119 
objectlogics (e.g. package isabelleHOL). 
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 higherorder 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 firstorder 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 ZermeloFraenkel 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, wellfounded 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 simplytyped 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 hardwired 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  HigherOrder Logic 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

160 
Group: Applications/Math 
6567  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 objectlogic for Isabelle. 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

164 

7312  165 
%package HOLReal 
166 
Summary: Isabelle Theorem Proving Environment  HigherOrder Logic 

167 
Group: Applications/Math 

168 
Requires: isabelle 

169 
%description HOLReal 

170 
This package contains a binary image of the HOL objectlogic for Isabelle, 

171 
including support for real numbers. 

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  ZermeloFraenkel set theory 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

175 
Group: Applications/Math 
6567  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 objectlogic for Isabelle. 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

179 

7488  180 
%package pdfdocs 
181 
Summary: Isabelle Theorem Proving Environment  PDF documentation 

182 
Group: Applications/Math 

183 
Requires: isabelle 

184 
%description pdfdocs 

185 
This package contains the Isabelle documentation in PDF. Note that 

186 
the dvi version is already part of the base package. 

187 

7312  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  195 
%post 
196 
\$RPM_INSTALL_PREFIX/$ISABELLE_NAME/bin/isatool install p $BIN 

197 

198 
%post HOL 

199 
%post HOLReal 

200 
%post ZF 

7488  201 
%post pdfdocs 
7312  202 

203 
%postun 

204 
rm f $BIN/Isabelle $BIN/isabelle $BIN/isatool 

205 

206 
%postun HOL 

207 
%postun HOLReal 

208 
%postun ZF 

7488  209 
%postun pdfdocs 
7312  210 

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  215 
%files HOLReal 
216 
$ISABELLE_HOME/heaps/${COMPILER}/HOLReal 

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  221 
%files pdfdocs 
222 
EOF 

223 

224 
for F in $(ls 1 doc/*.pdf); do 

225 
echo "$ISABELLE_HOME/$F" >>$TMP/SPECS/isabelle.spec 

226 
done 

227 

228 

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  231 
%dir $ISABELLE_HOME 
7488  232 
%dir $ISABELLE_HOME/doc 
7337  233 
%dir $ISABELLE_HOME/heaps 
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  237 
for F in $(ls 1  grep v heaps  grep v browser_info  grep v doc); do 
238 
echo "$ISABELLE_HOME/$F" >>$TMP/SPECS/isabelle.spec 

239 
done 

240 

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  248 
chown R root:root "$TMP"  chgrp R isabelle "$TMP" 
6495  249 

8046  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  253 
cd /usr/src/packages/RPMS/i386 
254 
mv "isabelle$RPMVERSION${RPMRELEASE}.i386.rpm" "$DISTBASE/rpm/isabelle.rpm" 

255 
mv "isabelleHOL$RPMVERSION${RPMRELEASE}.i386.rpm" "$DISTBASE/rpm/isabelleHOL.i386.rpm" 

256 
mv "isabelleHOLReal$RPMVERSION${RPMRELEASE}.i386.rpm" "$DISTBASE/rpm/isabelleHOLReal.i386.rpm" 

257 
mv "isabelleZF$RPMVERSION${RPMRELEASE}.i386.rpm" "$DISTBASE/rpm/isabelleZF.i386.rpm" 

258 
mv "isabellepdfdocs$RPMVERSION${RPMRELEASE}.i386.rpm" "$DISTBASE/rpm/isabellepdfdocs.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" 