[packages/coq] - updated dependencies, added doc and sse2 bconds
qboosh
qboosh at pld-linux.org
Sat Jan 22 20:34:12 CET 2022
commit 10fd38a7b035fe4eaa1e0d17344bf2418fdf0642
Author: Jakub Bogusz <qboosh at pld-linux.org>
Date: Sat Jan 22 20:35:24 2022 +0100
- updated dependencies, added doc and sse2 bconds
coq.spec | 59 +++++++++++++++++++++++++++++++++++++++++------------------
1 file changed, 41 insertions(+), 18 deletions(-)
---
diff --git a/coq.spec b/coq.spec
index 83a7e87..f8073b5 100644
--- a/coq.spec
+++ b/coq.spec
@@ -1,8 +1,14 @@
#
# Conditional build:
-%bcond_without ocaml_opt # skip building native optimized binaries (bytecode is always built)
+%bcond_without ocaml_opt # native optimized binaries (bytecode is always built)
+%bcond_with sse2 # SSE2 instructions
+%bcond_with doc # documentation
%bcond_with tests # run testsuite (csdp dependant micromega tests fail badly on x86_64)
#
+%ifarch pentium4 %{x8664} x32
+%define with_sse2 1
+%endif
+
%ifnarch %{ix86} %{x8664} %{arm} aarch64 ppc sparc sparcv9
%undefine with_ocaml_opt
%endif
@@ -18,18 +24,27 @@ Source0: https://github.com/coq/coq/archive/V%{version}/%{name}-%{version}.tar.g
# Source0-md5: 03ebbf1034c224a0a3327db2d5688c29
Source1: coqide.desktop
Source2: coqide.xpm
-URL: http://coq.inria.fr/
+URL: https://coq.inria.fr/
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: ocaml-lablgtk3-devel >= 3.1.0
+BuildRequires: ocaml-lablgtk3-gtksourceview-devel >= 3.1.0
BuildRequires: sed >= 4.0
+%if %{with doc}
+BuildRequires: python3 >= 1:3
+# TODO (and adjust package name)
+BuildRequires: python3-antlr4-python3-runtime >= 4.7.1
+BuildRequires: python3-bs4 >= 4.0.6
+BuildRequires: python3-pexpect >= 4.2.1
+BuildRequires: python3-sphinx_rtd_theme >= 0.4.3
+# TODO (and adjust package name)
+BuildRequires: python3-sphinxcontrib-bibtex >= 0.4.2
+BuildRequires: sphinx-pdg >= 2.3.1
+# TODO: update texlive packages list (or drop pdf building leaving only html)
BuildRequires: texlive-fonts-cmextra
BuildRequires: texlive-fonts-cmsuper
BuildRequires: texlive-fonts-other
@@ -42,6 +57,10 @@ BuildRequires: texlive-makeindex
BuildRequires: texlive-psutils
# hyperref.sty (from latex) requires ifxexex.sty (from xetex)
BuildRequires: texlive-xetex
+%endif
+%if %{with sse2}
+Requires: cpuinfo(sse2)
+%endif
%requires_eq ocaml-runtime
Obsoletes: coq-emacs < 8.13.1
# same as ocaml-zarith
@@ -69,22 +88,25 @@ Coq to narzędzie pomagające w udowadnianiu, które:
jego formalnej specyfikacji.
%package latex
-Summary: Coq documentation style for latex
-Summary(pl.UTF-8): Styl dokumentacji Coq dla latexa
+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.
+Coq documentation style for LaTeX.
%description latex -l pl.UTF-8
-Styl dokumentacji Coq dla latexa.
+Styl dokumentacji Coq dla LaTeXa.
%prep
%setup -q
%{__sed} -ri '/FULLCONFIGDIR/s/OLDROOT|COQINSTALLPREFIX/&2/g' Makefile.install
%{__sed} -i 's|-Wall.*-O2|%{rpmcflags} -Wno-unused|' configure.ml
+%if %{with sse2}
+%{__sed} -i -e '/cflags_sse2/ s/-msse2 -mfpmath=sse//' configure.ml
+%endif
%{__sed} -i "s|-oc|-ccopt '%{rpmldflags}' -g &|" Makefile.build
%{__sed} -i 's,-shared,& -g,g' tools/CoqMakefile.in Makefile.build
@@ -99,21 +121,22 @@ Styl dokumentacji Coq dla latexa.
%build
./configure \
-bindir %{_bindir} \
- -libdir %{_libdir}/coq \
- -mandir %{_mandir} \
- -docdir %{_docdir}/%{name}-%{version} \
-configdir %{_sysconfdir}/%{name} \
- -datadir %{_datadir}/%{name} \
-coqdocdir %{_datadir}/texmf/tex/latex/misc \
+ -datadir %{_datadir}/%{name} \
+ -docdir %{_docdir}/%{name}-%{version} \
+ -libdir %{_libdir}/coq \
+ -mandir %{_mandir} \
%if %{with ocaml_opt}
- -native-compiler yes \
-coqide opt \
+ -native-compiler yes \
%else
-byte-only \
- -native-compiler no \
-coqide byte \
+ -native-compiler no \
%endif
- -browser "xdg-open %s"
+ -browser "xdg-open %s" \
+ %{?with_doc:-with-doc yes}
%{__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
@@ -133,7 +156,7 @@ install -d $RPM_BUILD_ROOT{%{_desktopdir},%{_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}
+cp -p CONTRIBUTING.md CREDITS README.md $RPM_BUILD_ROOT%{_docdir}/%{name}-%{version}
%clean
rm -rf $RPM_BUILD_ROOT
================================================================
---- gitweb:
http://git.pld-linux.org/gitweb.cgi/packages/coq.git/commitdiff/10fd38a7b035fe4eaa1e0d17344bf2418fdf0642
More information about the pld-cvs-commit
mailing list