author  wenzelm 
Mon, 03 May 1999 10:51:44 +0200  
changeset 6562  ac091e18b9fc 
parent 6561  793b33191ce3 
child 6567  8338dd394144 
permissions  rwxrxrx 
6485
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

1 
#!/bin/bash 
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" 
6562  67 
( PATH=/bin:$PATH; ./configure ) 
6485
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

68 
./build b $LOGICS 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

69 
./bin/isatool install d "$ISABELLE_HOME" p "$TMP/BUILD$BIN" 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

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

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

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

74 

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

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

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

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

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

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

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

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

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

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

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

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

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

89 

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

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

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

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

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

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

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

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

97 
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

98 
Packager: Markus Wenzel <wenzelm@in.tum.de> 
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 

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

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

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

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

148 
Requires: %{name} = %{version} 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

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

150 
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

151 

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

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

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

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

155 
Requires: %{name} = %{version} 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

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

157 
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

158 

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

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

162 

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

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

164 

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

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

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

167 

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

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

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

170 

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

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

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

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

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

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

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

177 

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

178 
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

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

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

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

182 

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

185 

6561  186 
chown R root:root "$TMP"  chgrp R isabelle "$TMP" 
6495  187 

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

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

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

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

193 
cp "isabelle$RPMVERSION1.i386.rpm" "$DISTBASE/rpm/isabelle.rpm" 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

194 
cp "isabelleHOL$RPMVERSION1.i386.rpm" "$DISTBASE/rpm/isabelleHOL.i386.rpm" 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

195 
cp "isabelleZF$RPMVERSION1.i386.rpm" "$DISTBASE/rpm/isabelleZF.i386.rpm" 
0d334465f29a
make Isabelle rpm packages for Linux/x86 from the distribution;
wenzelm
parents:
diff
changeset

196 

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

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

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

199 
rm rf "$TMP" 