| | 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* |
projects / packages / coq.git / blame_incremental