author  wenzelm 
Fri, 01 Sep 2000 17:36:42 +0200  
changeset 9781  32378f1c2f17 
parent 8853  079f607dc3dd 
child 9925  40f02ebcb3c0 
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" 
8853  11 
FAKE_BUILD="" 
6485
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

12 
DISTBASE=~/tmp/isadist 
6499  13 
ROOT=/usr/share 
14 
BIN=/usr/bin 

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

42 

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

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/isabellemakerpm$$" 
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  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  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  77 
if [ n "$FAKE_BUILD" ]; then 
78 
mkdir p heaps/${COMPILER} 

79 
touch heaps/${COMPILER}/HOL 

80 
touch heaps/${COMPILER}/HOLReal 

81 
touch heaps/${COMPILER}/ZF 

82 
else 

83 
./build bi $LOGICS 

84 
rm f heaps/${COMPILER}/Pure heaps/${COMPILER}/FOL heaps/${COMPILER}/TLA 

85 
fi 

8046  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  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  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  121 
the ML compiler and any of the precompiled Isabelle objectlogics 
122 
(e.g. package isabelleHOL). 

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

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

167 

7312  168 
%package HOLReal 
169 
Summary: Isabelle Theorem Proving Environment  HigherOrder Logic 

170 
Group: Applications/Math 

171 
Requires: isabelle 

172 
%description HOLReal 

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

174 
including support for real numbers. 

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

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

182 

7488  183 
%package pdfdocs 
184 
Summary: Isabelle Theorem Proving Environment  PDF documentation 

185 
Group: Applications/Math 

186 
Requires: isabelle 

187 
%description pdfdocs 

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

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

190 

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

200 

201 
%post HOL 

202 
%post HOLReal 

203 
%post ZF 

7488  204 
%post pdfdocs 
7312  205 

206 
%postun 

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

208 

209 
%postun HOL 

210 
%postun HOLReal 

211 
%postun ZF 

7488  212 
%postun pdfdocs 
7312  213 

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

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  224 
%files pdfdocs 
225 
EOF 

226 

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

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

229 
done 

230 

231 

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  234 
%dir $ISABELLE_HOME 
7488  235 
%dir $ISABELLE_HOME/doc 
7337  236 
%dir $ISABELLE_HOME/heaps 
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  240 
for F in $(ls 1  grep v heaps  grep v browser_info  grep v doc); do 
241 
echo "$ISABELLE_HOME/$F" >>$TMP/SPECS/isabelle.spec 

242 
done 

243 

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

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

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

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

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

261 
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

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" 