# 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

# 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 core-source
Summary:        Source files of the Rocq Prelude, and the Corelib and Ltac2 modules
Requires:       %{name}-core%{?_isa} = %{version}-%{release}

%description core-source %_desc

This package contains the source Rocq files for the Rocq Prelude, and the
Corelib and Ltac2 modules.  These files are not needed to use the Rocq Prelude,
and the Corelib and Ltac2 modules.  They are made available for informational
purposes.

%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

cat .ofiles-coq-core .ofiles-coq-core-devel > .ofiles-coq-core-all
cat .ofiles-rocqide  .ofiles-rocqide-devel  > .ofiles-rocqide-all

cat .ofiles-coq-core-devel
cat .ofiles-rocqide-devel

%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
%{ocamldir}/rocq-core/
%{ocamldir}/coq
%exclude %{ocamldir}/coq/theories/*/*.v
%exclude %{ocamldir}/coq/user-contrib/Ltac2/*/*.v

%files core-source
%{ocamldir}/coq/theories/*/*.v
%{ocamldir}/coq/user-contrib/Ltac2/*/*.v

%files -n coq-core-compat -f .ofiles-coq-core-all

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

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

%files rocqide -f .ofiles-rocqide-all
%doc ide/rocqide/FAQ
%{_datadir}/icons/hicolor/256x256/apps/rocq.png
%{_datadir}/icons/hicolor/256x256/mimetypes/rocqfile.png
%{_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