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

# This package is installed into an archful location, but contains no ELF
# objects.
%global debug_package %{nil}

# 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 stdlibdir %{ocamldir}/coq/user-contrib/Stdlib
%global rocqver   9.1.0
%global giturl    https://github.com/rocq-prover/stdlib

Name:           rocq-stdlib
Version:        9.0.0
Release:        %autorelease
Summary:        The Rocq proof assistant standard library

License:        LGPL-2.1-only
URL:            https://rocq-prover.org/
VCS:            git:%{giturl}.git
Source0:        %{giturl}/archive/V%{version}/%{name}-%{version}.tar.gz

BuildRequires:  rocq = %{rocqver}
BuildRequires:  coq-core-compat
BuildRequires:  ocaml >= 4.09.0
BuildRequires:  ocaml-dune >= 3.6.1
BuildRequires:  ocaml-findlib

Requires:       rocq%{?_isa} = %{rocqver}

# 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

This package includes the Rocq Standard Library, that is to say, the
set of modules usually bound to the Stdlib.* namespace.

%package source
Summary:        Source files of the Rocq proof assistant standard library
Requires:       %{name}%{?_isa} = %{version}-%{release}

%description source %_desc

This package contains the source Rocq files for the standard library.  These
files are not needed to use the standard library.  They are made available for
informational purposes.

%prep
%autosetup -n stdlib-%{version} -p1

%build
%dune_build -p rocq-stdlib

%install
%dune_install rocq-stdlib

%files
%doc README.md CONTRIBUTING.md
%license LICENSE
%{ocamldir}/%{name}/
%{stdlibdir}
%exclude %{stdlibdir}/*/*.v

%files source
%{stdlibdir}/*/*.v

%changelog
%autochangelog