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