# Rocq's plugin architecture requires cmxs files, so:
ExclusiveArch: %{ocaml_native_compiler}

# ANTLR is unavailable on i686
# See https://fedoraproject.org/wiki/Changes/Drop_i686_JDKs
#
# This is commented for out now because ocaml_native_compiler is
# narrower, and apparently if you have two ExclusiveArch lines in a
# spec file, RPM ignores the first one and uses the second one!
# ExclusiveArch: %%{java_arches}

%ifarch %{ocaml_native_compiler}
%global camlsuffix opt
%else
%global camlsuffix byte
%endif

# .coqide-gtk2rc produces an rpmlint warning due to its name,
# however, this name is proper as per the Rocq documentation

# Rocq installs python files into nonstandard places
%global _python_bytecompile_extra 0

# TESTING NOTE: The testsuite requires that rocq-stdlib be installed already.
# Hence, we cannot run it on the koji builders.  The maintainer should always
# install the package and run the test suite manually before committing (in a
# container, for example).  The following steps are required.
#
# Install all required packages:
#
#   rocq-core rocq-runtime rocq-stdlib rocq-coqide-server
#   ocaml ocaml-dune ocaml-findlib-devel ocaml-ocamldoc ocaml-ounit2-devel
#   make rsync time
#
# Run the tests from within the `test-suite' directory:
#
#   $ make -j2 BIN=/usr/bin/ ROCQLIB=/usr/lib64/ocaml/coq/
#
# Inspect any failing tests by printing the logs:
#
#   $ make report PRINT_LOGS=1

%global giturl  https://github.com/rocq-prover/rocq

Name:           rocq
Version:        9.1.0
Release:        %autorelease
Summary:        Proof management system

# The project as a whole is LGPL-2.1-only.  Exceptions:
# - clib/diff2.ml is MIT
# - gramlib is BSD-3-Clause
License:        LGPL-2.1-only AND MIT AND BSD-3-Clause
URL:            https://rocq-prover.org/
VCS:            git:%{giturl}.git
Source0:        %{giturl}/archive/V%{version}/%{name}-%{version}.tar.gz
Source1:        fr.inria.rocqide.desktop
Source2:        rocq.xml
Source3:        fr.inria.rocqide.metainfo.xml
# Expose a dependency on the math library so rpm can see it
Patch:          %{name}-mathlib.patch
# [Backport] Fix documentation build (upstream commit 17e4fb9).
Patch:          %{name}-no-generated-readme.patch

BuildRequires:  ocaml >= 4.09.0
BuildRequires:  ocaml-cairo-devel >= 0.6.4
BuildRequires:  ocaml-dune >= 3.6.1
BuildRequires:  ocaml-findlib-devel >= 1.8.1
BuildRequires:  ocaml-lablgtk3-sourceview3-devel >= 3.1.2
BuildRequires:  ocaml-ocamldoc
BuildRequires:  ocaml-ounit2-devel
BuildRequires:  ocaml-zarith-devel >= 1.11
BuildRequires:  adwaita-icon-theme
BuildRequires:  libappstream-glib
BuildRequires:  csdp-tools
BuildRequires:  desktop-file-utils
BuildRequires:  findutils
BuildRequires:  make
BuildRequires:  python3-devel

# For documentation
BuildRequires:  antlr4 >= 4.7.1
BuildRequires:  %{py3_dist antlr4-python3-runtime}
BuildRequires:  %{py3_dist beautifulsoup4}
BuildRequires:  %{py3_dist pexpect}
BuildRequires:  %{py3_dist sphinx}
BuildRequires:  %{py3_dist sphinxcontrib-bibtex}
BuildRequires:  %{py3_dist sphinx-rtd-theme}
Buildrequires:  python3-sphinx-latex
%if 0%{?fedora} < 44
BuildRequires:  latexmk
BuildRequires:  tex(ellipse.sty)
BuildRequires:  tex(fontawesome5.sty)
BuildRequires:  tex(pict2e.sty)
%endif
# Other dependencies
BuildRequires:  tex(adjustbox.sty)
BuildRequires:  tex(amsfonts.sty)
BuildRequires:  tex(amsmath.sty)
BuildRequires:  tex(amsmidx.sty)
BuildRequires:  tex(amssymb.sty)
BuildRequires:  tex(array.sty)
BuildRequires:  tex(babel.sty)
BuildRequires:  tex(fancyhdr.sty)
BuildRequires:  tex(fontenc.sty)
BuildRequires:  tex(fullpage.sty)
BuildRequires:  tex(hyperref.sty)
BuildRequires:  tex(ifpdf.sty)
BuildRequires:  tex(inputenc.sty)
BuildRequires:  tex(latin1.def)
BuildRequires:  tex(microtype.sty)
BuildRequires:  tex(polyglossia.sty)
BuildRequires:  tex(pslatex.sty)
BuildRequires:  tex(t1enc.def)
BuildRequires:  tex(tipa.sty)
BuildRequires:  tex(ucs.sty)
BuildRequires:  tex(unicode-math.sty)
BuildRequires:  tex(url.sty)
BuildRequires:  tex(utf8.def)
BuildRequires:  tex(utf8x.def)
BuildRequires:  tex(verbatim.sty)
BuildRequires:  tex(xr.sty)

Requires:       %{name}-runtime%{_isa} = %{version}-%{release}
Requires:       %{name}-core%{_isa} = %{version}-%{release}
Requires:       csdp-tools
Requires:       ocaml-findlib
Requires:       texlive-base

Recommends:     emacs-proofgeneral
Recommends:     rocq-stdlib

# This can be removed when F43 reaches EOL
Provides:       coq = %{version}-%{release}
Obsoletes:      coq < 9.1.0

%global _desc %{expand:
Rocq is a formal proof management system.  It provides a formal language
to write mathematical definitions, executable algorithms and theorems
together with an environment for semi-interactive development of
machine-checked proofs.}

%description %_desc

Typical applications include the certification of properties of
programming languages (e.g. the CompCert compiler certification project,
or the Bedrock verified low-level programming library), the formalization
of mathematics (e.g. the full formalization of the Feit-Thompson theorem
or homotopy type theory) and teaching.

%package runtime
Summary:        Core binaries and tools of the Rocq proof management system
Requires:       %{name}%{?_isa} = %{version}-%{release}
# This can be removed when F43 reaches EOL
Provides:       coq-core = %{version}-%{release}
Obsoletes:      coq-core < 9.1.0

%description runtime %_desc

This package includes the Rocq prover core binaries, plugins, and tools, but
not the vernacular standard library.

%package runtime-devel
Summary:        Development files for %{name}-runtime
Requires:       %{name}-runtime%{?_isa} = %{version}-%{release}

%description runtime-devel %_desc

The %{name}-runtime-devel package contains libraries and signature files
for developing applications that use %{name}-runtime.

%package core
Summary:        The Rocq Prelude, and the Corelib and Ltac2 modules
Requires:       %{name}-runtime%{?_isa} = %{version}-%{release}
# This can be removed when F43 reaches EOL
Provides:       coq = %{version}-%{release}
Obsoletes:      coq < 9.1.0

%description core %_desc

This package includes the Rocq prelude, that is loaded automatically
by Rocq in every .v file, as well as other modules bound to the
Corelib.* and Ltac2.* namespaces.

%package -n coq-core-compat
Summary:        Compatibility binaries for Coq after the Rocq renaming
Requires:       %{name}-core%{?_isa} = %{version}-%{release}
# This can be removed when F43 reaches EOL
Provides:       coq-core = %{version}-%{release}
Obsoletes:      coq-core < 9.1.0

%description -n coq-core-compat %_desc

This package includes compatibility binaries to call Rocq
through previous Coq commands like coqc coqtop,...

%package coqide-server
Summary:        The coqidetop language server
Requires:       %{name}-core%{?_isa} = %{version}-%{release}
# This can be removed when F43 reaches EOL
Provides:       coq-coqide-server = %{version}-%{release}
Obsoletes:      coq-coqide-server < 9.1.0

%description coqide-server %_desc

This package provides the coqidetop language server, an implementation of
Rocq's XML protocol which allows clients, such as RocqIDE, to interact with
Rocq in a structured way.

%package coqide-server-devel
Summary:        Development files for %{name}-coqide-server
Requires:       %{name}-coqide-server%{?_isa} = %{version}-%{release}

%description    coqide-server-devel %_desc

The %{name}-coqide-server-devel package contains libraries and signature files
for developing applications that use %{name}-coqide-server.

%package rocqide
Summary:        RocqIDE for the Rocq proof management system
Requires:       %{name}-coqide-server%{?_isa} = %{version}-%{release}
Requires:       adwaita-icon-theme
Requires:       hicolor-icon-theme
Requires:       xdg-utils
# This can be removed when F43 reaches EOL
Provides:       coq-coqide = %{version}-%{release}
Obsoletes:      coq-coqide < 9.1.0

%description rocqide %_desc

This package provides RocqIDE, a graphical user interface for the
development of interactive proofs.

%package doc
Summary:        Documentation for the Rocq proof management system
# The documentation as a whole is OPUBL-1.0.
# Some sphinx-installed files are LGPL-2.1-only.
# Some sphinx-installed files are MIT.
#
# The OPUBL-1.0 license is not allowed for Fedora, but carries this usage note
# (https://gitlab.com/fedora/legal/fedora-license-data/-/blob/main/data/OPUBL-1.0.toml):
# "Allowed-for documentation if the copyright holder does not exercise any of
# the “LICENSE OPTIONS” listed in Section VI".
#
# doc/LICENSE contains this note: "Options A and B are *not* elected."
#
# Therefore, this package falls under the Fedora exception.
License:        OPUBL-1.0 AND LGPL-2.1-only AND MIT
BuildArch:      noarch
Requires:       font(fontawesome)
Requires:       font(lato)
Requires:       font(robotoslab)
# This can be removed when F43 reaches EOL
Provides:       coq-doc = %{version}-%{release}
Obsoletes:      coq-doc < 9.1.0

%description doc %_desc

This package provides documentation and tutorials for the system.  The
main documentation comes in two parts: the main Library documentation,
which describes all Corelib.* modules, and the Reference Manual, which
gives a more complete description of the whole system. Included are
HTML versions of both and a PDF version of the Reference Manual.

%prep
%autosetup -p1

%conf
fixtimestamp() {
  touch -r $1.orig $1
  rm -f $1.orig
}

# Use Fedora flags
sed -e 's|-Wall.*-O2|%{build_cflags} %{build_ldflags} -Wno-unused|' \
    -e 's| -march=native||' \
    -i tools/configure/configure.ml

# Make sure debuginfo is generated
sed -i 's,-shared,& -g,g' tools/CoqMakefile.in

# Do not invoke env
for f in doc/tools/coqrst/notations/fontsupport.py;
do
  sed -i.orig 's,/usr/bin/env python2,%{python3},' $f
  fixtimestamp $f
done
for f in $(grep -Frl '%{_bindir}/env'); do
  sed -r -i.orig 's,(%{_bindir}/)env[[:blank:]]+([[:alnum:]]+),\1\2,g' $f
  fixtimestamp $f
done

%build
%global rocqdocdir %{?_pkgdocdir}%{!?_pkgdocdir:%{_docdir}/rocq-%{version}}

# Regenerate ANTLR files
cd doc/tools/coqrst/notations
antlr4 -Dlanguage=Python3 -visitor -no-listener TacticNotations.g
cd -

# Set our configuration options
# NOTE: Keep libdir `coq', it's hard-coded in Dune for `coq.theory' stanzas.
./configure -prefix %{_prefix}                       \
            -libdir %{ocamldir}/coq                  \
            -configdir %{_sysconfdir}/xdg/%{name}    \
            -mandir %{_mandir}                       \
            -docdir %{rocqdocdir}                    \
%ifarch %{ocaml_natdynlink}
            -natdynlink yes                          \
%else
            -natdynlink no                           \
%endif
            -browser "xdg-open %s"                   \
            -bytecode-compiler yes                   \
            -native-compiler no
# As of coq 8.17.0, the native compiler cannot be build with OCaml 5.x
#%%ifarch %%{ocaml_native_compiler}
#            -native-compiler yes
#%%else
#            -native-compiler no
#%%endif

# Build the binary artifacts
make dunestrap VERBOSE=1 DUNEOPT="--verbose --profile=release"
%dune_build -p rocq-runtime,rocq-core,coq-core,coqide-server,rocqide

# Build the documentation
export ROCQLIB=${PWD}/_build/install/default/lib/coq
export SPHINXWARNOPT="-w$PWD/sphinx-warn.log"
%dune_build @refman-html @refman-pdf @corelib-html

%install
%dune_install rocq-runtime rocq-core coq-core coqide-server rocqide

# Install the LaTeX style file
mkdir -p %{buildroot}%{_texmf_main}/tex/latex/misc
mv %{buildroot}%{_datadir}/texmf/tex/latex/misc/coqdoc.sty \
   %{buildroot}%{_texmf_main}/tex/latex/misc
rm -fr %{buildroot}%{_datadir}/texmf

# FIXME: dune ignores the configdir argument to configure
mkdir -p %{buildroot}%{_sysconfdir}/xdg/%{name}

# Prepare the documentation for installation
find _build/default/doc -name .buildinfo -delete

# Install the documentation
mkdir -p %{buildroot}%{rocqdocdir}/refman-pdf
mv _build/default/doc/refman-pdf/rocq*.pdf %{buildroot}%{rocqdocdir}/refman-pdf/
mv _build/default/doc/refman-html %{buildroot}%{rocqdocdir}/refman-html
mv _build/default/doc/corelib/html %{buildroot}%{rocqdocdir}/corelib
mv _build/default/doc/corelib/_index.html %{buildroot}%{rocqdocdir}/corelib/

# Install desktop and file type icons
mkdir -p %{buildroot}%{_datadir}/icons/hicolor/256x256/apps
mkdir -p %{buildroot}%{_datadir}/icons/hicolor/256x256/mimetypes
cp --preserve=timestamps ide/rocqide/coq.png \
   %{buildroot}%{_datadir}/icons/hicolor/256x256/apps/rocq.png
cp --preserve=timestamps ide/rocqide/coq.png \
   %{buildroot}%{_datadir}/icons/hicolor/256x256/mimetypes/rocqfile.png

# Make a MIME type for .v files
mkdir -p %{buildroot}%{_datadir}/mime/packages
cp -p %{SOURCE2} %{buildroot}%{_datadir}/mime/packages

# Install desktop file
desktop-file-install --dir=%{buildroot}%{_datadir}/applications %{SOURCE1}

# Install AppData file
mkdir -p %{buildroot}%{_metainfodir}
install -pm 644 %{SOURCE3} %{buildroot}%{_metainfodir}
appstream-util validate-relax --nonet \
  %{buildroot}%{_metainfodir}/fr.inria.rocqide.metainfo.xml

# Install the language bindings
# NOTE: Must still be installed in a dir named `coq'.
mkdir -p %{buildroot}%{_datadir}/gtksourceview-3.0/language-specs
for fil in coq.lang coq-ssreflect.lang; do
  ln -s ../../coq/$fil %{buildroot}%{_datadir}/gtksourceview-3.0/language-specs
done

# Install the style file
# NOTE: Must still be installed in a dir named `coq'.
mkdir -p %{buildroot}%{_datadir}/gtksourceview-3.0/styles
ln -s ../../coq/coq_style.xml %{buildroot}%{_datadir}/gtksourceview-3.0/styles

# Byte compile the tools
%py_byte_compile %{python3} %{buildroot}%{ocamldir}/coq-core/tools

# Generate file lists
%{ocaml_files -s}
ls -la

%files
# Empty metapackage.

%files runtime -f .ofiles-rocq-runtime
%doc README.md
%license LICENSE
%{_texmf_main}/tex/latex/misc/

%files runtime-devel -f .ofiles-rocq-runtime-devel

%files core -f .ofiles-rocq-core
%{ocamldir}/rocq-core/dune-package
%{ocamldir}/rocq-core/opam

%files -n coq-core-compat -f .ofiles-coq-core
%{ocamldir}/coq-core/dune-package
%{ocamldir}/ccq-core/opam

%files coqide-server -f .ofiles-coqide-server

%files coqide-server-devel -f .ofiles-coqide-server-devel

%files rocqide
%doc ide/rocqide/FAQ
# NOTE: Arch independent data is still stored in a dir named `coq'.
%{_datadir}/coq/
%{_datadir}/icons/hicolor/256x256/apps/rocq.png
%{_datadir}/icons/hicolor/256x256/mimetypes/rocqfile.png
%{_mandir}/man1/rocqide.1*
%{ocamldir}/rocqide/
%{_metainfodir}/fr.inria.rocqide.metainfo.xml
%{_datadir}/applications/fr.inria.rocqide.desktop
%{_datadir}/gtksourceview-3.0/language-specs/coq*.lang
%{_datadir}/gtksourceview-3.0/styles/coq_style.xml
%{_datadir}/mime/packages/rocq.xml
%{_sysconfdir}/xdg/rocq/

%files doc
%license doc/LICENSE
%{rocqdocdir}

%changelog
%autochangelog