#
# Conditional build:
%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

Summary:	The Coq Proof Assistant
Summary(pl.UTF-8):	Coq - narzędzie pomagające w udowadnianiu
Name:		coq
Version:	8.13.1
Release:	5
License:	LGPL v2.1
Group:		Applications/Math
Source0:	https://github.com/coq/coq/archive/V%{version}/%{name}-%{version}.tar.gz
# Source0-md5:	03ebbf1034c224a0a3327db2d5688c29
Source1:	coqide.desktop
Source2:	coqide.xpm
URL:		https://coq.inria.fr/
BuildRequires:	bash
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 >= 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
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
%endif
%if %{with sse2}
Requires:	cpuinfo(sse2)
%endif
%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,
 - 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 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

%{__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

%{__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} \
	-configdir %{_sysconfdir}/%{name} \
	-coqdocdir %{_datadir}/texmf/tex/latex/misc \
	-datadir %{_datadir}/%{name} \
	-docdir %{_docdir}/%{name}-%{version} \
	-libdir %{_libdir}/coq \
	-mandir %{_mandir} \
%if %{with ocaml_opt}
	-coqide opt \
	-native-compiler yes \
%else
	-byte-only \
	-coqide byte \
	-native-compiler no \
%endif
	-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

%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}

# 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 CREDITS README.md $RPM_BUILD_ROOT%{_docdir}/%{name}-%{version}

%clean
rm -rf $RPM_BUILD_ROOT

%files
%defattr(644,root,root,755)
%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}/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.opt
%attr(755,root,root) %{_bindir}/coqwc
%attr(755,root,root) %{_bindir}/coqworkmgr
%attr(755,root,root) %{_bindir}/ocamllibdep
%attr(755,root,root) %{_bindir}/votour
%dir %{_libdir}/coq
%{_libdir}/coq/*
%{_mandir}/man1/coq_makefile.1*
%{_mandir}/man1/coq-tex.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*
%{?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