author  wenzelm 
Mon, 06 Sep 1999 16:59:46 +0200  
changeset 7488  c49d17fac066 
parent 7337  3f8eeb0b6d75 
child 7992  6f49fe89bfe1 
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 

6485
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

14 

0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

15 

0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

16 
## diagnostics 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

17 

0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

18 
PRG=$(basename $0) 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

19 

0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

20 
function usage() 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

21 
{ 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

22 
echo 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

23 
echo "Usage: $PRG ARCHIVE" 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

24 
echo 
7488  25 
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

26 
echo 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

27 
exit 1 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

28 
} 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

29 

0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

30 
function fail() 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

31 
{ 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

32 
echo "$1" >&2 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

33 
exit 2 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

34 
} 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

35 

0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

36 

0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

37 
## process command line 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

38 

7488  39 
[ $# gt 1 ] && usage 
6485
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

40 

7488  41 
ARCHIVE="$1"; shift 
42 

6485
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

43 

0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

44 

0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

45 
## main 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

46 

0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

47 
[ ! f "$ARCHIVE" ] && fail "Bad archive file $ARCHIVE" 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

48 
ARCHIVE_BASE=$(basename "$ARCHIVE") 
7488  49 
ARCHIVE_DIR=$(cd $(dirname "$ARCHIVE"); echo $PWD) 
50 
ARCHIVE_FULL=$ARCHIVE_DIR/$ARCHIVE_BASE 

6485
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

51 

0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

52 
ISABELLE_NAME=$(basename "$ARCHIVE_BASE" .tar.gz) 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

53 
ISABELLE_HOME="$ROOT/$ISABELLE_NAME" 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

54 

7488  55 
PDF_ARCHIVE_FULL="$ARCHIVE_DIR/${ISABELLE_NAME}_pdf.tar.gz" 
56 
[ ! f "$PDF_ARCHIVE_FULL" ] && PDF_ARCHIVE_FULL="" 

57 

6485
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

58 

0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

59 
# prep 
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 
TMP="/tmp/isabellemakerpm$$" 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

62 
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

63 

0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

64 
cd "$TMP/BUILD$ROOT" 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

65 
tar xpzf "$ARCHIVE_FULL" 
7488  66 
[ 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

67 

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 
# build 
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 
cd "$TMP/BUILD$ROOT/$ISABELLE_NAME" 
7488  72 
( env BASH_PATH=/bin/bash PERL_PATH=/usr/bin/perl ./configure ) 
7312  73 
./build bi $LOGICS 
6485
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

74 
COMPILER=$(./bin/isatool getenv b ML_IDENTIFIER) 
7314  75 
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

76 

0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

77 

0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

78 
# rpm spec 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

79 

0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

80 
RPMVERSION=$(echo "$ISABELLE_NAME"  perl w \ 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

81 
e '$name = <STDIN>;' \ 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

82 
e 'if ($name =~ m/^Isabelle(\d+)$/) {' \ 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

83 
e ' $rpmversion = "$1";' \ 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

84 
e '} elsif ($name =~ m/^Isabelle(\d+)(\d+)$/) {' \ 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

85 
e ' $rpmversion = "$1p$2";' \ 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

86 
e '} elsif ($name =~ m/^Isabelle_(\d+)(\w+)(\d+)$/) {' \ 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

87 
e ' $rpmversion = "$1$2$3";' \ 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

88 
e '} else {' \ 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

89 
e ' $rpmversion = "";' \ 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

90 
e '};' \ 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

91 
e 'print $rpmversion;') 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

92 

0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

93 
[ 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

94 

0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

95 
cat >$TMP/SPECS/isabelle.spec <<EOF 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

96 
Summary: Isabelle Theorem Proving Environment 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

97 
Name: isabelle 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

98 
Version: $RPMVERSION 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

99 
Release: 1 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

100 
Group: Applications/Math 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

101 
Copyright: University of Cambridge Computer Laboratory 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

102 
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

103 
Packager: Markus Wenzel <wenzelm@in.tum.de> 
7312  104 
Prefix: $ROOT 
6485
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

105 
BuildRoot: $TMP/BUILD 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

106 

0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

107 
%description 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

108 

0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

109 
This package contains the full source distribution of Isabelle 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

110 
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

111 
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

112 
objectlogics (e.g. package isabelleHOL). 
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 

0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

115 
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

116 
Cambridge University (Larry Paulson) and TU Munich (Tobias Nipkow). 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

117 
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

118 
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

119 
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

120 
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

121 
applications. 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

122 

0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

123 
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

124 
other examples (see also the Isabelle theory library at 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

125 
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

126 
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

127 
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

128 
Functions (domain theory) to HOL. Isabelle/FOL provides basic 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

129 
classical and intuitionistic firstorder logic. It is polymorphic. 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

130 
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

131 
of FOL. 
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 
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

134 
an extensive library of (concrete) mathematics, and various packages 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

135 
for advanced definitional concepts (like (co)inductive sets and 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

136 
types, wellfounded recursion etc.). The distribution also includes 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

137 
some large applications, for example correctness proofs of 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

138 
cryptographic protocols (HOL/Auth) or communication protocols 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

139 
(HOLCF/IOA). 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

140 

0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

141 
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

142 
slightly less developed library. Its definitional packages are 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

143 
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

144 
constructions for sets than simplytyped HOL. 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

145 

0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

146 
Logics are not hardwired into Isabelle, but formulated within 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

147 
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

148 
syntactic and deductive tools available in generic Isabelle. Isabelle 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

149 
proof tools provide a high degree of automation. 
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 
%package HOL 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

152 
Summary: Isabelle Theorem Proving Environment  HigherOrder Logic 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

153 
Group: Applications/Math 
6567  154 
Requires: isabelle 
6485
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

155 
%description HOL 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

156 
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

157 

7312  158 
%package HOLReal 
159 
Summary: Isabelle Theorem Proving Environment  HigherOrder Logic 

160 
Group: Applications/Math 

161 
Requires: isabelle 

162 
%description HOLReal 

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

164 
including support for real numbers. 

165 

6485
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

166 
%package ZF 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

167 
Summary: Isabelle Theorem Proving Environment  ZermeloFraenkel set theory 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

168 
Group: Applications/Math 
6567  169 
Requires: isabelle 
6485
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

170 
%description ZF 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

171 
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

172 

7488  173 
%package pdfdocs 
174 
Summary: Isabelle Theorem Proving Environment  PDF documentation 

175 
Group: Applications/Math 

176 
Requires: isabelle 

177 
%description pdfdocs 

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

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

180 

7312  181 

6485
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

182 
%prep 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

183 

0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

184 
%build 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

185 

0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

186 
%install 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

187 

7312  188 
%post 
189 
\$RPM_INSTALL_PREFIX/$ISABELLE_NAME/bin/isatool install p $BIN 

190 

191 
%post HOL 

192 
%post HOLReal 

193 
%post ZF 

7488  194 
%post pdfdocs 
7312  195 

196 
%postun 

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

198 

199 
%postun HOL 

200 
%postun HOLReal 

201 
%postun ZF 

7488  202 
%postun pdfdocs 
7312  203 

204 

6485
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

205 
%files HOL 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

206 
$ISABELLE_HOME/heaps/${COMPILER}/HOL 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

207 

7312  208 
%files HOLReal 
209 
$ISABELLE_HOME/heaps/${COMPILER}/HOLReal 

210 

6485
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

211 
%files ZF 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

212 
$ISABELLE_HOME/heaps/${COMPILER}/ZF 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

213 

7488  214 
%files pdfdocs 
215 
EOF 

216 

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

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

219 
done 

220 

221 

222 
cat >>$TMP/SPECS/isabelle.spec <<EOF 

6485
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

223 
%files 
7337  224 
%dir $ISABELLE_HOME 
7488  225 
%dir $ISABELLE_HOME/doc 
7337  226 
%dir $ISABELLE_HOME/heaps 
227 
%dir $ISABELLE_HOME/heaps/${COMPILER} 

6485
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

228 
EOF 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

229 

7488  230 
for F in $(ls 1  grep v heaps  grep v browser_info  grep v doc); do 
231 
echo "$ISABELLE_HOME/$F" >>$TMP/SPECS/isabelle.spec 

232 
done 

233 

234 
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

235 
echo "$ISABELLE_HOME/$F" >>$TMP/SPECS/isabelle.spec 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

236 
done 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

237 

0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

238 

0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

239 
# invoke rpm 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

240 

6561  241 
chown R root:root "$TMP"  chgrp R isabelle "$TMP" 
6495  242 

6485
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

243 
echo "topdir: $TMP" >"$TMP/rpmrc" 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

244 
rpm rcfile "$TMP/rpmrc" bb "$TMP/SPECS/isabelle.spec" 
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 
mkdir p "$DISTBASE/rpm" 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

247 
cd "$TMP/RPMS/i386" 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

248 
cp "isabelle$RPMVERSION1.i386.rpm" "$DISTBASE/rpm/isabelle.rpm" 
7312  249 
cp "isabelleHOL$RPMVERSION1.i386.rpm" "$DISTBASE/rpm/isabelleHOL.i386.rpm" 
7314  250 
cp "isabelleHOLReal$RPMVERSION1.i386.rpm" "$DISTBASE/rpm/isabelleHOLReal.i386.rpm" 
7312  251 
cp "isabelleZF$RPMVERSION1.i386.rpm" "$DISTBASE/rpm/isabelleZF.i386.rpm" 
7488  252 
cp "isabellepdfdocs$RPMVERSION1.i386.rpm" "$DISTBASE/rpm/isabellepdfdocs.rpm" 
6485
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

253 

0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

254 
# clean up 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

255 
cd / 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

256 
rm rf "$TMP" 