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