]>
Commit | Line | Data |
---|---|---|
680764bb JR |
1 | # This file has been generated from RH/coq.spec.tpl |
2 | # Do not edit | |
3 | Name: coq | |
4 | Version: 7.4 | |
5 | Release: 1 | |
6 | Summary: The Coq Proof Assistant | |
7 | License: GPL | |
8 | Group: Applications/Math | |
9 | Vendor: INRIA Rocquencourt | |
10 | URL: http://coq.inria.fr | |
11 | Source0: ftp://ftp.inria.fr/INRIA/coq/V7.4/%{name}-%{version}.tar.gz | |
12 | # Source0-md5: 13ac61f150823e54ad84a9096e2dd646 | |
235fb63c | 13 | Patch0: coq-ocaml-3.07.patch |
680764bb JR |
14 | Icon: petit-coq.gif |
15 | BuildRequires: ocaml | |
16 | BuildRequires: emacs | |
17 | BuildRoot: %{tmpdir}/%{name}-%{version}-root-%(id -u -n) | |
18 | ||
19 | %description | |
20 | Coq is a proof assistant which: | |
21 | - allows to handle calculus assertions, | |
22 | - check mechanically proofs of these assertions, | |
23 | - helps to find formal proofs, | |
24 | - extracts a certified program from the constructive proof of its | |
25 | formal specification, | |
26 | ||
27 | %prep | |
28 | %setup -q | |
235fb63c | 29 | %patch0 -p0 |
680764bb JR |
30 | |
31 | %build | |
32 | ./configure \ | |
33 | -bindir %{_bindir} \ | |
34 | -libdir %{_libdir}/coq \ | |
35 | -mandir %{_mandir} \ | |
36 | -emacs emacs \ | |
37 | -emacslib %{_datadir}/emacs/site-lisp \ | |
38 | -opt \ | |
39 | -reals all # Need ocamlc.opt and ocamlopt.opt | |
40 | ||
41 | %{__make} world check # Use native coq to compile theories | |
42 | ||
43 | %install | |
44 | rm -rf $RPM_BUILD_ROOT | |
45 | %{__make} -e COQINSTALLPREFIX=$RPM_BUILD_ROOT/ install | |
46 | # To install only locally the binaries compiled with absolute paths | |
47 | ||
48 | %clean | |
49 | rm -rf $RPM_BUILD_ROOT | |
50 | ||
51 | %files | |
52 | %defattr(644,root,root,755) | |
53 | %attr(755,root,root) %{_bindir}/coqmktop | |
54 | %attr(755,root,root) %{_bindir}/coqc | |
55 | %attr(755,root,root) %{_bindir}/coqtop.byte | |
56 | %attr(755,root,root) %{_bindir}/coqtop.opt | |
57 | %attr(755,root,root) %{_bindir}/coqtop | |
58 | %attr(755,root,root) %{_bindir}/coqdep | |
59 | %attr(755,root,root) %{_bindir}/gallina | |
60 | %attr(755,root,root) %{_bindir}/coq_makefile | |
61 | %attr(755,root,root) %{_bindir}/coq-tex | |
62 | %attr(755,root,root) %{_bindir}/coq-interface | |
63 | %attr(755,root,root) %{_bindir}/coq-interface.opt | |
64 | %attr(755,root,root) %{_bindir}/parser | |
65 | %attr(755,root,root) %{_bindir}/coq_vo2xml | |
66 | %{_libdir}/coq/theories/Init/Datatypes.vo | |
67 | %{_libdir}/coq/theories/Init/DatatypesSyntax.vo | |
68 | %{_libdir}/coq/theories/Init/Peano.vo | |
69 | %{_libdir}/coq/theories/Init/PeanoSyntax.vo | |
70 | %{_libdir}/coq/theories/Init/Logic.vo | |
71 | %{_libdir}/coq/theories/Init/Specif.vo | |
72 | %{_libdir}/coq/theories/Init/LogicSyntax.vo | |
73 | %{_libdir}/coq/theories/Init/SpecifSyntax.vo | |
74 | %{_libdir}/coq/theories/Init/Logic_Type.vo | |
75 | %{_libdir}/coq/theories/Init/Wf.vo | |
76 | %{_libdir}/coq/theories/Init/Logic_TypeSyntax.vo | |
77 | %{_libdir}/coq/theories/Init/Prelude.vo | |
78 | %{_libdir}/coq/theories/Logic/Hurkens.vo | |
79 | %{_libdir}/coq/theories/Logic/ProofIrrelevance.vo | |
80 | %{_libdir}/coq/theories/Logic/Classical.vo | |
81 | %{_libdir}/coq/theories/Logic/Classical_Type.vo | |
82 | %{_libdir}/coq/theories/Logic/Classical_Pred_Set.vo | |
83 | %{_libdir}/coq/theories/Logic/Eqdep.vo | |
84 | %{_libdir}/coq/theories/Logic/Classical_Pred_Type.vo | |
85 | %{_libdir}/coq/theories/Logic/Classical_Prop.vo | |
86 | %{_libdir}/coq/theories/Logic/ClassicalFacts.vo | |
87 | %{_libdir}/coq/theories/Logic/Berardi.vo | |
88 | %{_libdir}/coq/theories/Logic/Eqdep_dec.vo | |
89 | %{_libdir}/coq/theories/Logic/Decidable.vo | |
90 | %{_libdir}/coq/theories/Logic/JMeq.vo | |
91 | %{_libdir}/coq/theories/Arith/Arith.vo | |
92 | %{_libdir}/coq/theories/Arith/Gt.vo | |
93 | %{_libdir}/coq/theories/Arith/Between.vo | |
94 | %{_libdir}/coq/theories/Arith/Le.vo | |
95 | %{_libdir}/coq/theories/Arith/Compare.vo | |
96 | %{_libdir}/coq/theories/Arith/Lt.vo | |
97 | %{_libdir}/coq/theories/Arith/Compare_dec.vo | |
98 | %{_libdir}/coq/theories/Arith/Min.vo | |
99 | %{_libdir}/coq/theories/Arith/Div2.vo | |
100 | %{_libdir}/coq/theories/Arith/Minus.vo | |
101 | %{_libdir}/coq/theories/Arith/Mult.vo | |
102 | %{_libdir}/coq/theories/Arith/Even.vo | |
103 | %{_libdir}/coq/theories/Arith/EqNat.vo | |
104 | %{_libdir}/coq/theories/Arith/Peano_dec.vo | |
105 | %{_libdir}/coq/theories/Arith/Euclid.vo | |
106 | %{_libdir}/coq/theories/Arith/Plus.vo | |
107 | %{_libdir}/coq/theories/Arith/Wf_nat.vo | |
108 | %{_libdir}/coq/theories/Arith/Max.vo | |
109 | %{_libdir}/coq/theories/Arith/Bool_nat.vo | |
110 | %{_libdir}/coq/theories/Bool/Bool.vo | |
111 | %{_libdir}/coq/theories/Bool/IfProp.vo | |
112 | %{_libdir}/coq/theories/Bool/Zerob.vo | |
113 | %{_libdir}/coq/theories/Bool/DecBool.vo | |
114 | %{_libdir}/coq/theories/Bool/Sumbool.vo | |
115 | %{_libdir}/coq/theories/Bool/BoolEq.vo | |
116 | %{_libdir}/coq/theories/Bool/Bvector.vo | |
117 | %{_libdir}/coq/theories/ZArith/Wf_Z.vo | |
118 | %{_libdir}/coq/theories/ZArith/Zsyntax.vo | |
119 | %{_libdir}/coq/theories/ZArith/ZArith.vo | |
120 | %{_libdir}/coq/theories/ZArith/auxiliary.vo | |
121 | %{_libdir}/coq/theories/ZArith/ZArith_dec.vo | |
122 | %{_libdir}/coq/theories/ZArith/fast_integer.vo | |
123 | %{_libdir}/coq/theories/ZArith/Zmisc.vo | |
124 | %{_libdir}/coq/theories/ZArith/zarith_aux.vo | |
125 | %{_libdir}/coq/theories/ZArith/Zhints.vo | |
126 | %{_libdir}/coq/theories/ZArith/Zlogarithm.vo | |
127 | %{_libdir}/coq/theories/ZArith/Zpower.vo | |
128 | %{_libdir}/coq/theories/ZArith/Zcomplements.vo | |
129 | %{_libdir}/coq/theories/ZArith/Zdiv.vo | |
130 | %{_libdir}/coq/theories/ZArith/Zsqrt.vo | |
131 | %{_libdir}/coq/theories/ZArith/Zwf.vo | |
132 | %{_libdir}/coq/theories/ZArith/ZArith_base.vo | |
133 | %{_libdir}/coq/theories/ZArith/Zbool.vo | |
134 | %{_libdir}/coq/theories/ZArith/Zbinary.vo | |
135 | %{_libdir}/coq/theories/Lists/List.vo | |
136 | %{_libdir}/coq/theories/Lists/PolyListSyntax.vo | |
137 | %{_libdir}/coq/theories/Lists/ListSet.vo | |
138 | %{_libdir}/coq/theories/Lists/Streams.vo | |
139 | %{_libdir}/coq/theories/Lists/PolyList.vo | |
140 | %{_libdir}/coq/theories/Lists/TheoryList.vo | |
141 | %{_libdir}/coq/theories/Sets/Classical_sets.vo | |
142 | %{_libdir}/coq/theories/Sets/Permut.vo | |
143 | %{_libdir}/coq/theories/Sets/Constructive_sets.vo | |
144 | %{_libdir}/coq/theories/Sets/Powerset.vo | |
145 | %{_libdir}/coq/theories/Sets/Cpo.vo | |
146 | %{_libdir}/coq/theories/Sets/Powerset_Classical_facts.vo | |
147 | %{_libdir}/coq/theories/Sets/Ensembles.vo | |
148 | %{_libdir}/coq/theories/Sets/Powerset_facts.vo | |
149 | %{_libdir}/coq/theories/Sets/Finite_sets.vo | |
150 | %{_libdir}/coq/theories/Sets/Relations_1.vo | |
151 | %{_libdir}/coq/theories/Sets/Finite_sets_facts.vo | |
152 | %{_libdir}/coq/theories/Sets/Relations_1_facts.vo | |
153 | %{_libdir}/coq/theories/Sets/Image.vo | |
154 | %{_libdir}/coq/theories/Sets/Relations_2.vo | |
155 | %{_libdir}/coq/theories/Sets/Infinite_sets.vo | |
156 | %{_libdir}/coq/theories/Sets/Relations_2_facts.vo | |
157 | %{_libdir}/coq/theories/Sets/Integers.vo | |
158 | %{_libdir}/coq/theories/Sets/Relations_3.vo | |
159 | %{_libdir}/coq/theories/Sets/Multiset.vo | |
160 | %{_libdir}/coq/theories/Sets/Relations_3_facts.vo | |
161 | %{_libdir}/coq/theories/Sets/Partial_Order.vo | |
162 | %{_libdir}/coq/theories/Sets/Uniset.vo | |
163 | %{_libdir}/coq/theories/IntMap/Adalloc.vo | |
164 | %{_libdir}/coq/theories/IntMap/Mapcanon.vo | |
165 | %{_libdir}/coq/theories/IntMap/Addec.vo | |
166 | %{_libdir}/coq/theories/IntMap/Mapcard.vo | |
167 | %{_libdir}/coq/theories/IntMap/Addr.vo | |
168 | %{_libdir}/coq/theories/IntMap/Mapc.vo | |
169 | %{_libdir}/coq/theories/IntMap/Adist.vo | |
170 | %{_libdir}/coq/theories/IntMap/Mapfold.vo | |
171 | %{_libdir}/coq/theories/IntMap/Allmaps.vo | |
172 | %{_libdir}/coq/theories/IntMap/Mapiter.vo | |
173 | %{_libdir}/coq/theories/IntMap/Fset.vo | |
174 | %{_libdir}/coq/theories/IntMap/Maplists.vo | |
175 | %{_libdir}/coq/theories/IntMap/Lsort.vo | |
176 | %{_libdir}/coq/theories/IntMap/Mapsubset.vo | |
177 | %{_libdir}/coq/theories/IntMap/Mapaxioms.vo | |
178 | %{_libdir}/coq/theories/IntMap/Map.vo | |
179 | %{_libdir}/coq/theories/Relations/Newman.vo | |
180 | %{_libdir}/coq/theories/Relations/Operators_Properties.vo | |
181 | %{_libdir}/coq/theories/Relations/Relation_Definitions.vo | |
182 | %{_libdir}/coq/theories/Relations/Relation_Operators.vo | |
183 | %{_libdir}/coq/theories/Relations/Relations.vo | |
184 | %{_libdir}/coq/theories/Relations/Rstar.vo | |
185 | %{_libdir}/coq/theories/Wellfounded/Disjoint_Union.vo | |
186 | %{_libdir}/coq/theories/Wellfounded/Inclusion.vo | |
187 | %{_libdir}/coq/theories/Wellfounded/Inverse_Image.vo | |
188 | %{_libdir}/coq/theories/Wellfounded/Lexicographic_Exponentiation.vo | |
189 | %{_libdir}/coq/theories/Wellfounded/Transitive_Closure.vo | |
190 | %{_libdir}/coq/theories/Wellfounded/Union.vo | |
191 | %{_libdir}/coq/theories/Wellfounded/Wellfounded.vo | |
192 | %{_libdir}/coq/theories/Wellfounded/Well_Ordering.vo | |
193 | %{_libdir}/coq/theories/Wellfounded/Lexicographic_Product.vo | |
194 | %{_libdir}/coq/theories/Reals/TypeSyntax.vo | |
195 | %{_libdir}/coq/theories/Reals/Rdefinitions.vo | |
196 | %{_libdir}/coq/theories/Reals/Rsyntax.vo | |
197 | %{_libdir}/coq/theories/Reals/Raxioms.vo | |
198 | %{_libdir}/coq/theories/Reals/RIneq.vo | |
199 | %{_libdir}/coq/theories/Reals/DiscrR.vo | |
200 | %{_libdir}/coq/theories/Reals/Rbase.vo | |
201 | %{_libdir}/coq/theories/Reals/R_Ifp.vo | |
202 | %{_libdir}/coq/theories/Reals/Rbasic_fun.vo | |
203 | %{_libdir}/coq/theories/Reals/R_sqr.vo | |
204 | %{_libdir}/coq/theories/Reals/SplitAbsolu.vo | |
205 | %{_libdir}/coq/theories/Reals/SplitRmult.vo | |
206 | %{_libdir}/coq/theories/Reals/ArithProp.vo | |
207 | %{_libdir}/coq/theories/Reals/Rfunctions.vo | |
208 | %{_libdir}/coq/theories/Reals/Rseries.vo | |
209 | %{_libdir}/coq/theories/Reals/SeqProp.vo | |
210 | %{_libdir}/coq/theories/Reals/Rcomplete.vo | |
211 | %{_libdir}/coq/theories/Reals/PartSum.vo | |
212 | %{_libdir}/coq/theories/Reals/AltSeries.vo | |
213 | %{_libdir}/coq/theories/Reals/Binomial.vo | |
214 | %{_libdir}/coq/theories/Reals/Rsigma.vo | |
215 | %{_libdir}/coq/theories/Reals/Rprod.vo | |
216 | %{_libdir}/coq/theories/Reals/Cauchy_prod.vo | |
217 | %{_libdir}/coq/theories/Reals/Alembert.vo | |
218 | %{_libdir}/coq/theories/Reals/SeqSeries.vo | |
219 | %{_libdir}/coq/theories/Reals/Rtrigo_fun.vo | |
220 | %{_libdir}/coq/theories/Reals/Rtrigo_def.vo | |
221 | %{_libdir}/coq/theories/Reals/Rtrigo_alt.vo | |
222 | %{_libdir}/coq/theories/Reals/Cos_rel.vo | |
223 | %{_libdir}/coq/theories/Reals/Cos_plus.vo | |
224 | %{_libdir}/coq/theories/Reals/Rtrigo.vo | |
225 | %{_libdir}/coq/theories/Reals/Rlimit.vo | |
226 | %{_libdir}/coq/theories/Reals/Rderiv.vo | |
227 | %{_libdir}/coq/theories/Reals/RList.vo | |
228 | %{_libdir}/coq/theories/Reals/Ranalysis1.vo | |
229 | %{_libdir}/coq/theories/Reals/Ranalysis2.vo | |
230 | %{_libdir}/coq/theories/Reals/Ranalysis3.vo | |
231 | %{_libdir}/coq/theories/Reals/Rtopology.vo | |
232 | %{_libdir}/coq/theories/Reals/MVT.vo | |
233 | %{_libdir}/coq/theories/Reals/PSeries_reg.vo | |
234 | %{_libdir}/coq/theories/Reals/Exp_prop.vo | |
235 | %{_libdir}/coq/theories/Reals/Rtrigo_reg.vo | |
236 | %{_libdir}/coq/theories/Reals/Rsqrt_def.vo | |
237 | %{_libdir}/coq/theories/Reals/R_sqrt.vo | |
238 | %{_libdir}/coq/theories/Reals/Rtrigo_calc.vo | |
239 | %{_libdir}/coq/theories/Reals/Rgeom.vo | |
240 | %{_libdir}/coq/theories/Reals/Sqrt_reg.vo | |
241 | %{_libdir}/coq/theories/Reals/Ranalysis4.vo | |
242 | %{_libdir}/coq/theories/Reals/Rpower.vo | |
243 | %{_libdir}/coq/theories/Reals/Ranalysis.vo | |
244 | %{_libdir}/coq/theories/Reals/NewtonInt.vo | |
245 | %{_libdir}/coq/theories/Reals/RiemannInt_SF.vo | |
246 | %{_libdir}/coq/theories/Reals/RiemannInt.vo | |
247 | %{_libdir}/coq/theories/Reals/Integration.vo | |
248 | %{_libdir}/coq/theories/Reals/Reals.vo | |
249 | %{_libdir}/coq/theories/Setoids/Setoid.vo | |
250 | %{_libdir}/coq/theories/Sorting/Heap.vo | |
251 | %{_libdir}/coq/theories/Sorting/Permutation.vo | |
252 | %{_libdir}/coq/theories/Sorting/Sorting.vo | |
253 | %{_libdir}/coq/contrib/omega/Omega.vo | |
254 | %{_libdir}/coq/contrib/romega/ReflOmegaCore.vo | |
255 | %{_libdir}/coq/contrib/romega/ROmega.vo | |
256 | %{_libdir}/coq/contrib/ring/ArithRing.vo | |
257 | %{_libdir}/coq/contrib/ring/Ring_normalize.vo | |
258 | %{_libdir}/coq/contrib/ring/Ring_theory.vo | |
259 | %{_libdir}/coq/contrib/ring/Ring.vo | |
260 | %{_libdir}/coq/contrib/ring/ZArithRing.vo | |
261 | %{_libdir}/coq/contrib/ring/Ring_abstract.vo | |
262 | %{_libdir}/coq/contrib/ring/Quote.vo | |
263 | %{_libdir}/coq/contrib/ring/Setoid_ring_normalize.vo | |
264 | %{_libdir}/coq/contrib/ring/Setoid_ring.vo | |
265 | %{_libdir}/coq/contrib/ring/Setoid_ring_theory.vo | |
266 | %{_libdir}/coq/contrib/field/Field_Compl.vo | |
267 | %{_libdir}/coq/contrib/field/Field_Theory.vo | |
268 | %{_libdir}/coq/contrib/field/Field_Tactic.vo | |
269 | %{_libdir}/coq/contrib/field/Field.vo | |
270 | %{_libdir}/coq/contrib/correctness/Arrays.vo | |
271 | %{_libdir}/coq/contrib/correctness/Correctness.vo | |
272 | %{_libdir}/coq/contrib/correctness/Exchange.vo | |
273 | %{_libdir}/coq/contrib/correctness/ArrayPermut.vo | |
274 | %{_libdir}/coq/contrib/correctness/ProgBool.vo | |
275 | %{_libdir}/coq/contrib/correctness/ProgInt.vo | |
276 | %{_libdir}/coq/contrib/correctness/Sorted.vo | |
277 | %{_libdir}/coq/contrib/correctness/Tuples.vo | |
278 | %{_libdir}/coq/contrib/fourier/Fourier_util.vo | |
279 | %{_libdir}/coq/contrib/fourier/Fourier.vo | |
280 | %{_libdir}/coq/contrib/interface/Centaur.vo | |
281 | %{_libdir}/coq/contrib/cc/CC.vo | |
282 | %{_libdir}/coq/states/barestate.coq | |
283 | %{_libdir}/coq/states/initial.coq | |
284 | %{_datadir}/emacs/site-lisp/coq.el | |
285 | %{_datadir}/emacs/site-lisp/coq-inferior.el | |
286 | %{_mandir}/man1/coq-tex.1* | |
287 | %{_mandir}/man1/coqdep.1* | |
288 | %{_mandir}/man1/gallina.1* | |
289 | %{_mandir}/man1/coqc.1* | |
290 | %{_mandir}/man1/coqtop.1* | |
291 | %{_mandir}/man1/coqtop.byte.1* | |
292 | %{_mandir}/man1/coqtop.opt.1* | |
293 | %{_mandir}/man1/coq_makefile.1* | |
294 | %{_mandir}/man1/coqmktop.1* | |
295 | %{_mandir}/man1/coq-interface.1* | |
296 | %{_mandir}/man1/parser.1* | |
297 | %{_mandir}/man1/coq_vo2xml.1* |