- add patch needed to build with ocaml 3.07
[packages/coq.git] / coq.spec
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
13 Patch0:         coq-ocaml-3.07.patch
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
29 %patch0 -p0
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*
This page took 0.06033 seconds and 4 git commands to generate.