author  wenzelm 
Sat, 21 Aug 1999 16:54:09 +0200  
changeset 7312  523fb2832b30 
parent 6608  927def00b1c6 
child 7314  d3968533692c 
permissions  rwxrxrx 
7312  1 
#!/bin/bash x 
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 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

25 
echo "Make Isabelle rpm packages for Linux/x86 from distribution ARCHIVE." 
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 

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

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

40 

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

41 
ARCHIVE="$1" 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

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

49 
ARCHIVE_FULL=$(cd $(dirname "$ARCHIVE"); echo $PWD)/$ARCHIVE_BASE 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

50 

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

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

52 
ISABELLE_HOME="$ROOT/$ISABELLE_NAME" 
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 

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

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

56 

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

57 
TMP="/tmp/isabellemakerpm$$" 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

58 
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

59 

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

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

61 
tar xpzf "$ARCHIVE_FULL" 
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 

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

64 
# build 
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/$ISABELLE_NAME" 
7312  67 
( PATH=/bin:$PATH; BASH_PATH=/bin/bash PERL_PATH=/usr/bin/perl ./configure ) 
68 
./build bi $LOGICS 

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

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

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

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

73 

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

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

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

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

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

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

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

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

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

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

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

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

85 
e 'print $rpmversion;') 
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 
[ 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

88 

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

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

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

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

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

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

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

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

96 
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

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

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

100 

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

101 
%description 
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 
This package contains the full source distribution of Isabelle 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

104 
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

105 
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

106 
objectlogics (e.g. package isabelleHOL). 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

107 

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

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

111 
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

112 
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

113 
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

114 
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

115 
applications. 
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 
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

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

119 
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

120 
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

121 
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

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

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

124 
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

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

126 

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

127 
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

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

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

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

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

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

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

134 

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

135 
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

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

137 
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

138 
constructions for sets than simplytyped HOL. 
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 
Logics are not hardwired into Isabelle, but formulated within 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

141 
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

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

143 
proof tools provide a high degree of automation. 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

144 

7312  145 

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

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

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

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

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

151 
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

152 

7312  153 

154 
%package HOLReal 

155 
Summary: Isabelle Theorem Proving Environment  HigherOrder Logic 

156 
Group: Applications/Math 

157 
Requires: isabelle 

158 
%description HOLReal 

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

160 
including support for real numbers. 

161 

162 

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

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

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

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

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

168 
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

169 

7312  170 

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

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

172 

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

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

174 

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

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

176 

7312  177 
%post 
178 
\$RPM_INSTALL_PREFIX/$ISABELLE_NAME/bin/isatool install p $BIN 

179 

180 
%post HOL 

181 
%post HOLReal 

182 
%post ZF 

183 

184 
%postun 

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

186 

187 
%postun HOL 

188 
%postun HOLReal 

189 
%postun ZF 

190 

191 

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

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

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

194 

7312  195 
%files HOLReal 
196 
$ISABELLE_HOME/heaps/${COMPILER}/HOLReal 

197 

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

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

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

200 

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

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

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

203 

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

204 
for F in $(ls 1  grep v heaps  grep v browser_info) 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

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

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

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

208 

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

209 

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

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

211 

6561  212 
chown R root:root "$TMP"  chgrp R isabelle "$TMP" 
6495  213 

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

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

215 
rpm rcfile "$TMP/rpmrc" bb "$TMP/SPECS/isabelle.spec" 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

216 

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

217 
mkdir p "$DISTBASE/rpm" 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

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

219 
cp "isabelle$RPMVERSION1.i386.rpm" "$DISTBASE/rpm/isabelle.rpm" 
7312  220 
cp "isabelleHOL$RPMVERSION1.i386.rpm" "$DISTBASE/rpm/isabelleHOL.i386.rpm" 
221 
cp "isabelleHOL$RPMVERSION1.i386.rpm" "$DISTBASE/rpm/isabelleHOLReal.i386.rpm" 

222 
cp "isabelleZF$RPMVERSION1.i386.rpm" "$DISTBASE/rpm/isabelleZF.i386.rpm" 

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

223 

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

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

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

226 
rm rf "$TMP" 