projects / packages / coq.git / blame
| Commit | Line | Data |
|---|---|---|
| 521adcea | 1 | Summary: The Coq Proof Assistant |
| 680764bb JR |
2 | Name: coq |
| 3 | Version: 7.4 | |
| 4 | Release: 1 | |
| 680764bb JR |
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 | |
| 235fb63c | 11 | Patch0: coq-ocaml-3.07.patch |
| 680764bb JR |
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 | |
| 235fb63c | 27 | %patch0 -p0 |
| 680764bb JR |
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* |