X-Git-Url: http://git.pld-linux.org/?p=packages%2Fcoq.git;a=blobdiff_plain;f=coq.spec;h=5219986940343a151c892b5d94ead9bea4ab3729;hp=417c2efcc67824945da93de92700bf2f0a71972c;hb=78adac8;hpb=229b1af51ffb5ea5505d9c98f0b7fefd8ca82da3 diff --git a/coq.spec b/coq.spec index 417c2ef..5219986 100644 --- a/coq.spec +++ b/coq.spec @@ -1,23 +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): Coq - narzêdzie pomagaj±ce w udowadnianiu +Summary(pl.UTF-8): Coq - narzędzie pomagające w udowadnianiu Name: coq -Version: 8.0pl2 -Release: 2 -License: GPL +Version: 8.13.1 +Release: 4 +License: LGPL v2.1 Group: Applications/Math -Vendor: INRIA Rocquencourt -Source0: ftp://ftp.inria.fr/INRIA/coq/V%{version}/%{name}-%{version}.tar.gz -# Source0-md5: 39ee0fed76e47a11de2f49e2c236ef79 -# ftp://ftp.inria.fr/INRIA/coq/V8.0pl2/patch-coq-8.0pl2-ocaml-3.09 -Patch0: %{name}-ocaml-3.09.patch -Patch1: %{name}-lablgtk26.patch +Source0: https://github.com/coq/coq/archive/V%{version}/%{name}-%{version}.tar.gz +# Source0-md5: 03ebbf1034c224a0a3327db2d5688c29 +Source1: coqide.desktop +Source2: coqide.xpm URL: http://coq.inria.fr/ -BuildRequires: emacs -BuildRequires: ocaml >= 3.09.0 -BuildRequires: ocaml-camlp4 -BuildRequires: ocaml-lablgtk2-devel >= 2.6.0 +BuildRequires: bash +BuildRequires: hevea +BuildRequires: netpbm-progs +BuildRequires: ocaml >= 1:4.05 +BuildRequires: camlp5 >= 5.01 +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-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, @@ -26,78 +59,123 @@ Coq is a proof assistant which: - extracts a certified program from the constructive proof of its formal specification. -%description -l pl -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. +%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 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 -p0 -%patch1 -p1 + +%{__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} \ - -emacs emacs \ - -emacslib %{_datadir}/emacs/site-lisp \ - -opt \ - --coqdocdir %{_datadir}/texmf/tex/latex/misc \ - --coqide opt \ - -reals all # Need ocamlc.opt and ocamlopt.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} 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} install \ + COQINSTALLPREFIX=$RPM_BUILD_ROOT%{_prefix} \ + COQINSTALLPREFIX2=$RPM_BUILD_ROOT%{_sysconfdir} \ + OLDROOT=%{_prefix} \ + OLDROOT2=%{_sysconfdir} -%{__make} -e install \ - COQINSTALLPREFIX=$RPM_BUILD_ROOT/ # To install only locally the binaries compiled with absolute paths +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.byte -%attr(755,root,root) %{_bindir}/coqide.opt -%attr(755,root,root) %{_bindir}/coqmktop +%attr(755,root,root) %{_bindir}/coqide* +%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* +%{_desktopdir}/coqide.desktop +%{_pixmapsdir}/coqide.xpm +%{_datadir}/%{name} + +%files latex +%defattr(644,root,root,755) %{_datadir}/texmf/tex/latex/misc/coqdoc.sty