X-Git-Url: http://git.pld-linux.org/?p=packages%2Fcoq.git;a=blobdiff_plain;f=coq.spec;h=60c1ab9028c5a9b3c74a6d2b1bc119854e4b128d;hp=30829c8ca7a4e93cec0ec83cecfc153e7d6c2201;hb=3809f5d;hpb=308e751128d4e2072cc036d05a8758f26b0e2a2c diff --git a/coq.spec b/coq.spec index 30829c8..60c1ab9 100644 --- a/coq.spec +++ b/coq.spec @@ -1,30 +1,56 @@ +# +# 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 Summary(pl.UTF-8): Coq - narzędzie pomagające w udowadnianiu Name: coq -Version: 8.3pl1 -Release: 0.1 -License: GPL +Version: 8.13.1 +Release: 2 +License: LGPL v2.1 Group: Applications/Math -Vendor: INRIA Rocquencourt -Source0: http://coq.inria.fr/V%{version}/files/%{name}-%{version}.tar.gz -# Source0-md5: 1869d22b337f5da59ba3bbe1433f9a3b +Source0: https://github.com/coq/coq/archive/V%{version}/%{name}-%{version}.tar.gz +# Source0-md5: 03ebbf1034c224a0a3327db2d5688c29 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: ocaml >= 1:4.05 BuildRequires: camlp5 >= 5.01 -BuildRequires: ocaml-lablgtk2-devel >= 2.12.0 +BuildRequires: ocaml-dune > 2.5.0 +BuildRequires: ocaml-findlib >= 1.8.1 +BuildRequires: ocaml-zarith-devel >= 1.10 +BuildRequires: ocaml-lablgtk3-devel +BuildRequires: ocaml-lablgtk3-gtksourceview-devel 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-format-pdflatex +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 +Obsoletes: coq-emacs < 8.13.1 +# same as ocaml-zarith +ExclusiveArch: %{ix86} %{x8664} %{arm} aarch64 ppc sparc sparcv9 BuildRoot: %{tmpdir}/%{name}-%{version}-root-%(id -u -n) +# Exclude private ocaml interfaces +%define _noautoreq ocamlx?\\\((Configwin_types|Interface|Richpp|Serialize|Xml_p(arser|rinter)|Xmlprotocol)\\\) + %description Coq is a proof assistant which: - allows to handle calculus assertions, @@ -39,79 +65,117 @@ Coq to narzędzie pomagające w udowadnianiu, które: 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. +- wyciągać program o dowiedzionej poprawności z konstruktywnego dowodu + jego formalnej specyfikacji. + +%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} -ri '/FULLCONFIGDIR/s/OLDROOT|COQINSTALLPREFIX/&2/g' Makefile.install +%{__sed} -i 's|-Wall.*-O2|%{rpmcflags} -Wno-unused|' configure.ml +%{__sed} -i "s|-oc|-ccopt '%{rpmldflags}' -g &|" Makefile.build +%{__sed} -i 's,-shared,& -g,g' tools/CoqMakefile.in Makefile.build + +%{__sed} -E -i -e '1s,#!\s*/usr/bin/env\s+python3(\s|$),#!%{__python3}\1,' \ + tools/make-both-single-timing-files.py \ + tools/make-both-time-files.py \ + tools/make-one-time-file.py + +%{__sed} -E -i -e '1s,#!\s*/usr/bin/env\s+python2(\s|$),#!%{__python3}\1,' \ + doc/tools/coqrst/notations/fontsupport.py %build ./configure \ -bindir %{_bindir} \ -libdir %{_libdir}/coq \ -mandir %{_mandir} \ - -docdir %{_datadir}/coq/doc \ - -emacs emacs \ - -browser 'iceweasel -remote "OpenURL(%s,new-tab)" || iceweasel %s &' \ - -emacslib %{_datadir}/emacs/site-lisp \ - -opt \ - --coqdocdir %{_datadir}/texmf/tex/latex/misc \ - --coqide opt + -docdir %{_docdir}/%{name}-%{version} \ + -configdir %{_sysconfdir}/%{name} \ + -datadir %{_datadir}/%{name} \ + -coqdocdir %{_datadir}/texmf/tex/latex/misc \ +%if %{with ocaml_opt} + -native-compiler yes \ + -coqide opt \ +%else + -byte-only \ + -native-compiler no \ + -coqide byte \ +%endif + -browser "xdg-open %s" -%{__make} -j1 world check # Use native coq to compile theories +%{__make} world VERBOSE=1 CAML_LD_LIBRARY_PATH=kernel/byterun +%{?with_tests:%{__make} check VERBOSE=1 CAML_LD_LIBRARY_PATH=kernel/byterun} # Use native coq to compile theories %install rm -rf $RPM_BUILD_ROOT install -d $RPM_BUILD_ROOT{%{_desktopdir},%{_pixmapsdir}} -%{__make} -e install \ - COQINSTALLPREFIX=$RPM_BUILD_ROOT/ +%{__make} install \ + COQINSTALLPREFIX=$RPM_BUILD_ROOT%{_prefix} \ + COQINSTALLPREFIX2=$RPM_BUILD_ROOT%{_sysconfdir} \ + OLDROOT=%{_prefix} \ + OLDROOT2=%{_sysconfdir} + # To install only locally the binaries compiled with absolute paths -install %{SOURCE1} $RPM_BUILD_ROOT%{_desktopdir} -install %{SOURCE2} $RPM_BUILD_ROOT%{_pixmapsdir} +cp -p %{SOURCE1} $RPM_BUILD_ROOT%{_desktopdir} +cp -p %{SOURCE2} $RPM_BUILD_ROOT%{_pixmapsdir} + +cp -p CONTRIBUTING.md README.md $RPM_BUILD_ROOT%{_docdir}/%{name}-%{version} %clean rm -rf $RPM_BUILD_ROOT %files %defattr(644,root,root,755) -%attr(755,root,root) %{_bindir}/coq-interface -%attr(755,root,root) %{_bindir}/coq-interface.opt -%attr(755,root,root) %{_bindir}/coq-tex -%attr(755,root,root) %{_bindir}/coq_makefile +%doc %{_docdir}/%{name}-%{version} +%dir %{_sysconfdir}/%{name} %attr(755,root,root) %{_bindir}/coqc +%attr(755,root,root) %{_bindir}/coqchk %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}/coq_makefile +%attr(755,root,root) %{_bindir}/coqpp +%attr(755,root,root) %{_bindir}/coqproofworker.opt +%attr(755,root,root) %{_bindir}/coqqueryworker.opt +%attr(755,root,root) %{_bindir}/coqtacticworker.opt +%attr(755,root,root) %{_bindir}/coq-tex %attr(755,root,root) %{_bindir}/coqtop -%attr(755,root,root) %{_bindir}/coqtop.byte %attr(755,root,root) %{_bindir}/coqtop.opt %attr(755,root,root) %{_bindir}/coqwc -%attr(755,root,root) %{_bindir}/gallina -%attr(755,root,root) %{_bindir}/parser -%attr(755,root,root) %{_bindir}/parser.opt +%attr(755,root,root) %{_bindir}/coqworkmgr +%attr(755,root,root) %{_bindir}/ocamllibdep +%attr(755,root,root) %{_bindir}/votour %dir %{_libdir}/coq %{_libdir}/coq/* -%{_datadir}/emacs/site-lisp/coq.el -%{_datadir}/emacs/site-lisp/coq-inferior.el +%{_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/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/coqdoc.1* +%{?with_ocaml_opt:%{_mandir}/man1/coqtop.opt.1*} %{_mandir}/man1/coqwc.1* -%{_datadir}/texmf/tex/latex/misc/coqdoc.sty %{_desktopdir}/coqide.desktop %{_pixmapsdir}/coqide.xpm +%{_datadir}/%{name} + +%files latex +%defattr(644,root,root,755) +%{_datadir}/texmf/tex/latex/misc/coqdoc.sty