# 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} # The documentation package cannot be built with ocaml-dune 3.8.2. Check later # releases of both rocq and dune to see if the issues have been resolved. %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} %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