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