The package rpms/flocq.git has added or updated architecture specific content in its
spec file (ExclusiveArch/ExcludeArch or %ifarch/%ifnarch) in commit(s):
https://src.fedoraproject.org/cgit/rpms/flocq.git/commit/?id=98306bdce981....
Change:
+%ifarch %{ocaml_native_compiler}
Thanks.
Full change:
============
commit 98306bdce981090d2e4f96b5a4e01f60a98470bf
Author: Jerry James <loganjerry(a)gmail.com>
Date: Wed Mar 25 12:48:35 2020 -0600
Rebuild for coq 8.11.0.
diff --git a/flocq.rpmlintrc b/flocq.rpmlintrc
new file mode 100644
index 0000000..99ba92b
--- /dev/null
+++ b/flocq.rpmlintrc
@@ -0,0 +1,20 @@
+# THIS FILE IS FOR WHITELISTING RPMLINT ERRORS AND WARNINGS IN TASKOTRON
+#
https://fedoraproject.org/wiki/Taskotron/Tasks/dist.rpmlint#Whitelisting_...
+
+# The dictionary is missing some technical terms
+addFilter(r'W: spelling-error .* radix')
+
+# These directories are present on purpose on platforms with a native OCaml
+addFilter(r'W: hidden-file-or-dir .*\.coq-native')
+
+# This is effectively a devel package
+addFilter(r'flocq\.[^:]+: W: devel-file-in-non-devel-package')
+
+# The sources are just sources
+addFilter(r'flocq-source\.[^:]+: W: only-non-binary-in-usr-lib')
+
+# Documentation is in the main package
+addFilter(r'flocq-source\.[^:]+: W: no-documentation')
+
+# The configure script is not generated by autotools
+addFilter(r'flocq\.spec:[^:]+: W: configure-without-libdir-spec')
diff --git a/flocq.spec b/flocq.spec
index eb64d71..92bf59d 100644
--- a/flocq.spec
+++ b/flocq.spec
@@ -1,12 +1,17 @@
-# This package is really noarch, but it has to be installed in an arch-specific
-# location, so we build it as an arch-specific package.
+# On platforms with a native OCaml compiler, proofs can be compiled into cmxs
+# files, but there are no source files that rpm recognizes as such.
+%ifarch %{ocaml_native_compiler}
+%global _debugsource_template %{nil}
+%else
%global debug_package %{nil}
+%endif
+
%global flocqdir %{_libdir}/coq/user-contrib/Flocq
-%global coqver 8.9.1
+%global coqver 8.11.0
Name: flocq
Version: 3.2.0
-Release: 5%{?dist}
+Release: 6%{?dist}
Summary: Formalization of floating point numbers for Coq
License: LGPLv3+
@@ -16,6 +21,8 @@ Source0:
https://gforge.inria.fr/frs/download.php/file/38103/%{name}-%{ve
BuildRequires: gcc-c++
BuildRequires: remake
BuildRequires: coq = %{coqver}
+BuildRequires: ocaml
+BuildRequires: ocaml-findlib
Requires: coq%{?_isa} = %{coqver}
%description
@@ -36,6 +43,11 @@ purposes.
%prep
%setup -q
+# Force native compilation when available
+%ifarch %{ocaml_native_compiler}
+sed -i 's/@COQC@ -R src Flocq/& -native-compiler yes/' Remakefile.in
+%endif
+
%build
# We do NOT want to specify --libdir, and we don't need CFLAGS, etc.
./configure
@@ -73,6 +85,9 @@ cp -p src/Prop/*.v $RPM_BUILD_ROOT%{flocqdir}/Prop
%{flocqdir}/Prop/*.v
%changelog
+* Mon Mar 23 2020 Jerry James <loganjerry(a)gmail.com> - 3.2.0-6
+- Rebuild for coq 8.11.0
+
* Tue Jan 28 2020 Fedora Release Engineering <releng(a)fedoraproject.org> - 3.2.0-5
- Rebuilt for
https://fedoraproject.org/wiki/Fedora_32_Mass_Rebuild