X-Git-Url: http://git.pld-linux.org/?p=packages%2Fcoq.git;a=blobdiff_plain;f=coq.spec;h=3c2e76d8c84fa4c13e3af8299f9b7e25128b8fa2;hp=d3637af9286278d70c1211d5e3fabfa711d12a3c;hb=0e56eeb;hpb=680764bb92823c0b93706e4f55cbddd55f1cf06e diff --git a/coq.spec b/coq.spec index d3637af..3c2e76d 100644 --- a/coq.spec +++ b/coq.spec @@ -1,295 +1,181 @@ -# This file has been generated from RH/coq.spec.tpl -# Do not edit -Name: coq -Version: 7.4 -Release: 1 +# +# TODO: +# - package and R: Csdp (https://projects.coin-or.org/Csdp) +# +# Conditional build: +%bcond_without ocaml_opt # skip building native optimized binaries (bytecode is always built) +%bcond_with tests # run testsuite (csdp dependant micromega tests fail badly on x86_64) +# +%ifnarch %{ix86} %{x8664} arm aarch64 ppc sparc sparcv9 +%undefine with_ocaml_opt +%endif + Summary: The Coq Proof Assistant -License: GPL +Summary(pl.UTF-8): Coq - narzędzie pomagające w udowadnianiu +Name: coq +Version: 8.4pl6 +Release: 2 +License: LGPL v2.1 Group: Applications/Math -Vendor: INRIA Rocquencourt -URL: http://coq.inria.fr -Source0: ftp://ftp.inria.fr/INRIA/coq/V7.4/%{name}-%{version}.tar.gz -# Source0-md5: 13ac61f150823e54ad84a9096e2dd646 -Icon: petit-coq.gif -BuildRequires: ocaml +Source0: http://coq.inria.fr/distrib/V%{version}/files/%{name}-%{version}.tar.gz +# Source0-md5: 2334a98b64578cb81d2b4127e327b368 +Source1: coqide.desktop +Source2: coqide.xpm +Patch0: %{name}-lablgtk2.patch +URL: http://coq.inria.fr/ +BuildRequires: bash BuildRequires: emacs +BuildRequires: hevea +BuildRequires: netpbm-progs +BuildRequires: ocaml >= 3.09.0 +BuildRequires: camlp5 >= 5.01 +BuildRequires: ocaml-lablgtk2-devel >= 2.12.0 +BuildRequires: sed >= 4.0 +BuildRequires: texlive-fonts-cmextra +BuildRequires: texlive-fonts-cmsuper +BuildRequires: texlive-fonts-other +BuildRequires: texlive-format-pdflatex +BuildRequires: texlive-latex-ams +BuildRequires: texlive-latex-comment +BuildRequires: texlive-latex-moreverb +BuildRequires: texlive-latex-ucs +BuildRequires: texlive-makeindex +BuildRequires: texlive-psutils +# hyperref.sty (from latex) requires ifxexex.sty (from xetex) +BuildRequires: texlive-xetex +%requires_eq ocaml-runtime BuildRoot: %{tmpdir}/%{name}-%{version}-root-%(id -u -n) %description Coq is a proof assistant which: - - allows to handle calculus assertions, - - check mechanically proofs of these assertions, - - helps to find formal proofs, - - extracts a certified program from the constructive proof of its - formal specification, + - allows to handle calculus assertions, + - check mechanically proofs of these assertions, + - helps to find formal proofs, + - extracts a certified program from the constructive proof of its + formal specification. + +%description -l pl.UTF-8 +Coq to narzędzie pomagające w udowadnianiu, które: +- pozwala uporać się z twierdzeniami dotyczącymi rachunku + różniczkowego, +- mechanicznie sprawdzać dowody tych twierdzeń, +- pomagać w znalezieniu formalnych dowodów, +- wyciągać program o dowiedzionej poprawności z konstruktywnego + dowodu jego formalnej specyfikacji. + +%package emacs +Summary: Emacs mode and syntax for Coq +Summary(pl.UTF-8): Tryb i składnia Coq dla Emacsa +Group: Development/Tools +Requires: %{name} = %{version}-%{release} + +%description emacs +Emacs mode and suyntax files for Coq. + +%description emacs -l pl.UTF-8 +Pliki trybu i składni Coq dla Emacsa. + +%package latex +Summary: Coq documentation style for latex +Summary(pl.UTF-8): Styl dokumentacji Coq dla latexa +Group: Development/Tools +Requires: %{name} = %{version}-%{release} + +%description latex +Coq documentation style for latex. + +%description latex -l pl.UTF-8 +Styl dokumentacji Coq dla latexa. %prep %setup -q +%patch0 -p1 + +%{__sed} -i -e 's|#!/bin/sh|#!/bin/bash|' test-suite/check +%{__sed} -i -e 's|\(MAKE_TSOPTS=.*\) -s \(.*\)|\1 \2|' Makefile.build %build ./configure \ -bindir %{_bindir} \ -libdir %{_libdir}/coq \ -mandir %{_mandir} \ + -docdir %{_docdir}/%{name}-%{version} \ + -configdir %{_sysconfdir}/%{name} \ + -datadir %{_datadir}/%{name} \ -emacs emacs \ + -browser "xdg-open %s" \ -emacslib %{_datadir}/emacs/site-lisp \ - -opt \ - -reals all # Need ocamlc.opt and ocamlopt.opt + %{?with_ocaml_opt:-opt} \ + --coqdocdir %{_datadir}/texmf/tex/latex/misc \ + --coqide %{?with_ocaml_opt:opt}%{!?with_ocaml_opt:byte} -%{__make} world check # Use native coq to compile theories +%{__make} -j1 world VERBOSE=1 CAML_LD_LIBRARY_PATH=kernel/byterun +%{?with_tests:%{__make} -j1 check VERBOSE=1 CAML_LD_LIBRARY_PATH=kernel/byterun} # Use native coq to compile theories %install rm -rf $RPM_BUILD_ROOT -%{__make} -e COQINSTALLPREFIX=$RPM_BUILD_ROOT/ install +install -d $RPM_BUILD_ROOT{%{_desktopdir},%{_pixmapsdir}} + +%{__make} -e install \ + COQINSTALLPREFIX=$RPM_BUILD_ROOT/ # To install only locally the binaries compiled with absolute paths +install %{SOURCE1} $RPM_BUILD_ROOT%{_desktopdir} +install %{SOURCE2} $RPM_BUILD_ROOT%{_pixmapsdir} + +# pdf is enough +%{__rm} -r $RPM_BUILD_ROOT%{_docdir}/%{name}-%{version}/ps +cp -p CHANGES COMPATIBILITY COPYRIGHT CREDITS README $RPM_BUILD_ROOT%{_docdir}/%{name}-%{version} + %clean rm -rf $RPM_BUILD_ROOT %files %defattr(644,root,root,755) -%attr(755,root,root) %{_bindir}/coqmktop +%doc %{_docdir}/%{name}-%{version} +%dir %{_sysconfdir}/%{name} +%config(noreplace) %verify(not md5 mtime size) %{_sysconfdir}/%{name}/coqide-gtk2rc +%attr(755,root,root) %{_bindir}/coq_makefile +%attr(755,root,root) %{_bindir}/coq-tex %attr(755,root,root) %{_bindir}/coqc -%attr(755,root,root) %{_bindir}/coqtop.byte -%attr(755,root,root) %{_bindir}/coqtop.opt -%attr(755,root,root) %{_bindir}/coqtop +%attr(755,root,root) %{_bindir}/coqchk +%{?with_ocaml_opt:%attr(755,root,root) %{_bindir}/coqchk.opt} %attr(755,root,root) %{_bindir}/coqdep +%attr(755,root,root) %{_bindir}/coqdoc +%attr(755,root,root) %{_bindir}/coqide* +%attr(755,root,root) %{_bindir}/coqmktop +%attr(755,root,root) %{_bindir}/coqtop +%attr(755,root,root) %{_bindir}/coqtop.byte +%{?with_ocaml_opt:%attr(755,root,root) %{_bindir}/coqtop.opt} +%attr(755,root,root) %{_bindir}/coqwc %attr(755,root,root) %{_bindir}/gallina -%attr(755,root,root) %{_bindir}/coq_makefile -%attr(755,root,root) %{_bindir}/coq-tex -%attr(755,root,root) %{_bindir}/coq-interface -%attr(755,root,root) %{_bindir}/coq-interface.opt -%attr(755,root,root) %{_bindir}/parser -%attr(755,root,root) %{_bindir}/coq_vo2xml -%{_libdir}/coq/theories/Init/Datatypes.vo -%{_libdir}/coq/theories/Init/DatatypesSyntax.vo -%{_libdir}/coq/theories/Init/Peano.vo -%{_libdir}/coq/theories/Init/PeanoSyntax.vo -%{_libdir}/coq/theories/Init/Logic.vo -%{_libdir}/coq/theories/Init/Specif.vo -%{_libdir}/coq/theories/Init/LogicSyntax.vo -%{_libdir}/coq/theories/Init/SpecifSyntax.vo -%{_libdir}/coq/theories/Init/Logic_Type.vo -%{_libdir}/coq/theories/Init/Wf.vo -%{_libdir}/coq/theories/Init/Logic_TypeSyntax.vo -%{_libdir}/coq/theories/Init/Prelude.vo -%{_libdir}/coq/theories/Logic/Hurkens.vo -%{_libdir}/coq/theories/Logic/ProofIrrelevance.vo -%{_libdir}/coq/theories/Logic/Classical.vo -%{_libdir}/coq/theories/Logic/Classical_Type.vo -%{_libdir}/coq/theories/Logic/Classical_Pred_Set.vo -%{_libdir}/coq/theories/Logic/Eqdep.vo -%{_libdir}/coq/theories/Logic/Classical_Pred_Type.vo -%{_libdir}/coq/theories/Logic/Classical_Prop.vo -%{_libdir}/coq/theories/Logic/ClassicalFacts.vo -%{_libdir}/coq/theories/Logic/Berardi.vo -%{_libdir}/coq/theories/Logic/Eqdep_dec.vo -%{_libdir}/coq/theories/Logic/Decidable.vo -%{_libdir}/coq/theories/Logic/JMeq.vo -%{_libdir}/coq/theories/Arith/Arith.vo -%{_libdir}/coq/theories/Arith/Gt.vo -%{_libdir}/coq/theories/Arith/Between.vo -%{_libdir}/coq/theories/Arith/Le.vo -%{_libdir}/coq/theories/Arith/Compare.vo -%{_libdir}/coq/theories/Arith/Lt.vo -%{_libdir}/coq/theories/Arith/Compare_dec.vo -%{_libdir}/coq/theories/Arith/Min.vo -%{_libdir}/coq/theories/Arith/Div2.vo -%{_libdir}/coq/theories/Arith/Minus.vo -%{_libdir}/coq/theories/Arith/Mult.vo -%{_libdir}/coq/theories/Arith/Even.vo -%{_libdir}/coq/theories/Arith/EqNat.vo -%{_libdir}/coq/theories/Arith/Peano_dec.vo -%{_libdir}/coq/theories/Arith/Euclid.vo -%{_libdir}/coq/theories/Arith/Plus.vo -%{_libdir}/coq/theories/Arith/Wf_nat.vo -%{_libdir}/coq/theories/Arith/Max.vo -%{_libdir}/coq/theories/Arith/Bool_nat.vo -%{_libdir}/coq/theories/Bool/Bool.vo -%{_libdir}/coq/theories/Bool/IfProp.vo -%{_libdir}/coq/theories/Bool/Zerob.vo -%{_libdir}/coq/theories/Bool/DecBool.vo -%{_libdir}/coq/theories/Bool/Sumbool.vo -%{_libdir}/coq/theories/Bool/BoolEq.vo -%{_libdir}/coq/theories/Bool/Bvector.vo -%{_libdir}/coq/theories/ZArith/Wf_Z.vo -%{_libdir}/coq/theories/ZArith/Zsyntax.vo -%{_libdir}/coq/theories/ZArith/ZArith.vo -%{_libdir}/coq/theories/ZArith/auxiliary.vo -%{_libdir}/coq/theories/ZArith/ZArith_dec.vo -%{_libdir}/coq/theories/ZArith/fast_integer.vo -%{_libdir}/coq/theories/ZArith/Zmisc.vo -%{_libdir}/coq/theories/ZArith/zarith_aux.vo -%{_libdir}/coq/theories/ZArith/Zhints.vo -%{_libdir}/coq/theories/ZArith/Zlogarithm.vo -%{_libdir}/coq/theories/ZArith/Zpower.vo -%{_libdir}/coq/theories/ZArith/Zcomplements.vo -%{_libdir}/coq/theories/ZArith/Zdiv.vo -%{_libdir}/coq/theories/ZArith/Zsqrt.vo -%{_libdir}/coq/theories/ZArith/Zwf.vo -%{_libdir}/coq/theories/ZArith/ZArith_base.vo -%{_libdir}/coq/theories/ZArith/Zbool.vo -%{_libdir}/coq/theories/ZArith/Zbinary.vo -%{_libdir}/coq/theories/Lists/List.vo -%{_libdir}/coq/theories/Lists/PolyListSyntax.vo -%{_libdir}/coq/theories/Lists/ListSet.vo -%{_libdir}/coq/theories/Lists/Streams.vo -%{_libdir}/coq/theories/Lists/PolyList.vo -%{_libdir}/coq/theories/Lists/TheoryList.vo -%{_libdir}/coq/theories/Sets/Classical_sets.vo -%{_libdir}/coq/theories/Sets/Permut.vo -%{_libdir}/coq/theories/Sets/Constructive_sets.vo -%{_libdir}/coq/theories/Sets/Powerset.vo -%{_libdir}/coq/theories/Sets/Cpo.vo -%{_libdir}/coq/theories/Sets/Powerset_Classical_facts.vo -%{_libdir}/coq/theories/Sets/Ensembles.vo -%{_libdir}/coq/theories/Sets/Powerset_facts.vo -%{_libdir}/coq/theories/Sets/Finite_sets.vo -%{_libdir}/coq/theories/Sets/Relations_1.vo -%{_libdir}/coq/theories/Sets/Finite_sets_facts.vo -%{_libdir}/coq/theories/Sets/Relations_1_facts.vo -%{_libdir}/coq/theories/Sets/Image.vo -%{_libdir}/coq/theories/Sets/Relations_2.vo -%{_libdir}/coq/theories/Sets/Infinite_sets.vo -%{_libdir}/coq/theories/Sets/Relations_2_facts.vo -%{_libdir}/coq/theories/Sets/Integers.vo -%{_libdir}/coq/theories/Sets/Relations_3.vo -%{_libdir}/coq/theories/Sets/Multiset.vo -%{_libdir}/coq/theories/Sets/Relations_3_facts.vo -%{_libdir}/coq/theories/Sets/Partial_Order.vo -%{_libdir}/coq/theories/Sets/Uniset.vo -%{_libdir}/coq/theories/IntMap/Adalloc.vo -%{_libdir}/coq/theories/IntMap/Mapcanon.vo -%{_libdir}/coq/theories/IntMap/Addec.vo -%{_libdir}/coq/theories/IntMap/Mapcard.vo -%{_libdir}/coq/theories/IntMap/Addr.vo -%{_libdir}/coq/theories/IntMap/Mapc.vo -%{_libdir}/coq/theories/IntMap/Adist.vo -%{_libdir}/coq/theories/IntMap/Mapfold.vo -%{_libdir}/coq/theories/IntMap/Allmaps.vo -%{_libdir}/coq/theories/IntMap/Mapiter.vo -%{_libdir}/coq/theories/IntMap/Fset.vo -%{_libdir}/coq/theories/IntMap/Maplists.vo -%{_libdir}/coq/theories/IntMap/Lsort.vo -%{_libdir}/coq/theories/IntMap/Mapsubset.vo -%{_libdir}/coq/theories/IntMap/Mapaxioms.vo -%{_libdir}/coq/theories/IntMap/Map.vo -%{_libdir}/coq/theories/Relations/Newman.vo -%{_libdir}/coq/theories/Relations/Operators_Properties.vo -%{_libdir}/coq/theories/Relations/Relation_Definitions.vo -%{_libdir}/coq/theories/Relations/Relation_Operators.vo -%{_libdir}/coq/theories/Relations/Relations.vo -%{_libdir}/coq/theories/Relations/Rstar.vo -%{_libdir}/coq/theories/Wellfounded/Disjoint_Union.vo -%{_libdir}/coq/theories/Wellfounded/Inclusion.vo -%{_libdir}/coq/theories/Wellfounded/Inverse_Image.vo -%{_libdir}/coq/theories/Wellfounded/Lexicographic_Exponentiation.vo -%{_libdir}/coq/theories/Wellfounded/Transitive_Closure.vo -%{_libdir}/coq/theories/Wellfounded/Union.vo -%{_libdir}/coq/theories/Wellfounded/Wellfounded.vo -%{_libdir}/coq/theories/Wellfounded/Well_Ordering.vo -%{_libdir}/coq/theories/Wellfounded/Lexicographic_Product.vo -%{_libdir}/coq/theories/Reals/TypeSyntax.vo -%{_libdir}/coq/theories/Reals/Rdefinitions.vo -%{_libdir}/coq/theories/Reals/Rsyntax.vo -%{_libdir}/coq/theories/Reals/Raxioms.vo -%{_libdir}/coq/theories/Reals/RIneq.vo -%{_libdir}/coq/theories/Reals/DiscrR.vo -%{_libdir}/coq/theories/Reals/Rbase.vo -%{_libdir}/coq/theories/Reals/R_Ifp.vo -%{_libdir}/coq/theories/Reals/Rbasic_fun.vo -%{_libdir}/coq/theories/Reals/R_sqr.vo -%{_libdir}/coq/theories/Reals/SplitAbsolu.vo -%{_libdir}/coq/theories/Reals/SplitRmult.vo -%{_libdir}/coq/theories/Reals/ArithProp.vo -%{_libdir}/coq/theories/Reals/Rfunctions.vo -%{_libdir}/coq/theories/Reals/Rseries.vo -%{_libdir}/coq/theories/Reals/SeqProp.vo -%{_libdir}/coq/theories/Reals/Rcomplete.vo -%{_libdir}/coq/theories/Reals/PartSum.vo -%{_libdir}/coq/theories/Reals/AltSeries.vo -%{_libdir}/coq/theories/Reals/Binomial.vo -%{_libdir}/coq/theories/Reals/Rsigma.vo -%{_libdir}/coq/theories/Reals/Rprod.vo -%{_libdir}/coq/theories/Reals/Cauchy_prod.vo -%{_libdir}/coq/theories/Reals/Alembert.vo -%{_libdir}/coq/theories/Reals/SeqSeries.vo -%{_libdir}/coq/theories/Reals/Rtrigo_fun.vo -%{_libdir}/coq/theories/Reals/Rtrigo_def.vo -%{_libdir}/coq/theories/Reals/Rtrigo_alt.vo -%{_libdir}/coq/theories/Reals/Cos_rel.vo -%{_libdir}/coq/theories/Reals/Cos_plus.vo -%{_libdir}/coq/theories/Reals/Rtrigo.vo -%{_libdir}/coq/theories/Reals/Rlimit.vo -%{_libdir}/coq/theories/Reals/Rderiv.vo -%{_libdir}/coq/theories/Reals/RList.vo -%{_libdir}/coq/theories/Reals/Ranalysis1.vo -%{_libdir}/coq/theories/Reals/Ranalysis2.vo -%{_libdir}/coq/theories/Reals/Ranalysis3.vo -%{_libdir}/coq/theories/Reals/Rtopology.vo -%{_libdir}/coq/theories/Reals/MVT.vo -%{_libdir}/coq/theories/Reals/PSeries_reg.vo -%{_libdir}/coq/theories/Reals/Exp_prop.vo -%{_libdir}/coq/theories/Reals/Rtrigo_reg.vo -%{_libdir}/coq/theories/Reals/Rsqrt_def.vo -%{_libdir}/coq/theories/Reals/R_sqrt.vo -%{_libdir}/coq/theories/Reals/Rtrigo_calc.vo -%{_libdir}/coq/theories/Reals/Rgeom.vo -%{_libdir}/coq/theories/Reals/Sqrt_reg.vo -%{_libdir}/coq/theories/Reals/Ranalysis4.vo -%{_libdir}/coq/theories/Reals/Rpower.vo -%{_libdir}/coq/theories/Reals/Ranalysis.vo -%{_libdir}/coq/theories/Reals/NewtonInt.vo -%{_libdir}/coq/theories/Reals/RiemannInt_SF.vo -%{_libdir}/coq/theories/Reals/RiemannInt.vo -%{_libdir}/coq/theories/Reals/Integration.vo -%{_libdir}/coq/theories/Reals/Reals.vo -%{_libdir}/coq/theories/Setoids/Setoid.vo -%{_libdir}/coq/theories/Sorting/Heap.vo -%{_libdir}/coq/theories/Sorting/Permutation.vo -%{_libdir}/coq/theories/Sorting/Sorting.vo -%{_libdir}/coq/contrib/omega/Omega.vo -%{_libdir}/coq/contrib/romega/ReflOmegaCore.vo -%{_libdir}/coq/contrib/romega/ROmega.vo -%{_libdir}/coq/contrib/ring/ArithRing.vo -%{_libdir}/coq/contrib/ring/Ring_normalize.vo -%{_libdir}/coq/contrib/ring/Ring_theory.vo -%{_libdir}/coq/contrib/ring/Ring.vo -%{_libdir}/coq/contrib/ring/ZArithRing.vo -%{_libdir}/coq/contrib/ring/Ring_abstract.vo -%{_libdir}/coq/contrib/ring/Quote.vo -%{_libdir}/coq/contrib/ring/Setoid_ring_normalize.vo -%{_libdir}/coq/contrib/ring/Setoid_ring.vo -%{_libdir}/coq/contrib/ring/Setoid_ring_theory.vo -%{_libdir}/coq/contrib/field/Field_Compl.vo -%{_libdir}/coq/contrib/field/Field_Theory.vo -%{_libdir}/coq/contrib/field/Field_Tactic.vo -%{_libdir}/coq/contrib/field/Field.vo -%{_libdir}/coq/contrib/correctness/Arrays.vo -%{_libdir}/coq/contrib/correctness/Correctness.vo -%{_libdir}/coq/contrib/correctness/Exchange.vo -%{_libdir}/coq/contrib/correctness/ArrayPermut.vo -%{_libdir}/coq/contrib/correctness/ProgBool.vo -%{_libdir}/coq/contrib/correctness/ProgInt.vo -%{_libdir}/coq/contrib/correctness/Sorted.vo -%{_libdir}/coq/contrib/correctness/Tuples.vo -%{_libdir}/coq/contrib/fourier/Fourier_util.vo -%{_libdir}/coq/contrib/fourier/Fourier.vo -%{_libdir}/coq/contrib/interface/Centaur.vo -%{_libdir}/coq/contrib/cc/CC.vo -%{_libdir}/coq/states/barestate.coq -%{_libdir}/coq/states/initial.coq -%{_datadir}/emacs/site-lisp/coq.el -%{_datadir}/emacs/site-lisp/coq-inferior.el +%dir %{_libdir}/coq +%{_libdir}/coq/* +%{_mandir}/man1/coq_makefile.1* %{_mandir}/man1/coq-tex.1* -%{_mandir}/man1/coqdep.1* -%{_mandir}/man1/gallina.1* %{_mandir}/man1/coqc.1* +%{_mandir}/man1/coqchk.1* +%{_mandir}/man1/coqdep.1* +%{_mandir}/man1/coqdoc.1* +%{_mandir}/man1/coqide.1* +%{_mandir}/man1/coqmktop.1* %{_mandir}/man1/coqtop.1* %{_mandir}/man1/coqtop.byte.1* -%{_mandir}/man1/coqtop.opt.1* -%{_mandir}/man1/coq_makefile.1* -%{_mandir}/man1/coqmktop.1* -%{_mandir}/man1/coq-interface.1* -%{_mandir}/man1/parser.1* -%{_mandir}/man1/coq_vo2xml.1* +%{?with_ocaml_opt:%{_mandir}/man1/coqtop.opt.1*} +%{_mandir}/man1/coqwc.1* +%{_mandir}/man1/gallina.1* +%{_desktopdir}/coqide.desktop +%{_pixmapsdir}/coqide.xpm +%{_datadir}/%{name} + +%files emacs +%defattr(644,root,root,755) +%{_datadir}/emacs/site-lisp/coq.el +%{_datadir}/emacs/site-lisp/coq-db.el +%{_datadir}/emacs/site-lisp/coq-font-lock.el +%{_datadir}/emacs/site-lisp/coq-inferior.el +%{_datadir}/emacs/site-lisp/coq-syntax.el + +%files latex +%defattr(644,root,root,755) +%{_datadir}/texmf/tex/latex/misc/coqdoc.sty