OCaml 5.2.1 rebuild for Fedora 41

zenon-deprecated.patch

@@ -1,34 +0,0 @@
---- zenon-0.8.5/zenon_coqbool.v.orig	2020-10-23 09:19:07.000000000 -0600
-+++ zenon-0.8.5/zenon_coqbool.v	2026-03-03 16:33:33.636474063 -0700
-@@ -1,6 +1,6 @@
- (*  Copyright 2004 INRIA  *)
- 
--Require Export Bool.
-+From Stdlib Require Export Bool.
- 
- Definition __g_not_b := negb.
- Definition __g_and_b := andb.
---- zenon-0.8.5/zenon_focal.v.orig	2020-10-23 09:19:07.000000000 -0600
-+++ zenon-0.8.5/zenon_focal.v	2026-03-03 16:34:30.531982864 -0700
-@@ -1,8 +1,8 @@
- (*  Copyright 2004 INRIA  *)
- 
--Require Export Bool.
--Require Import ClassicalEpsilon.
--Require List.
-+From Stdlib Require Export Bool.
-+From Stdlib Require Import ClassicalEpsilon.
-+From Stdlib Require List.
- 
- (* magic: this whole file depends on the following definitions:
-    basics.and_b := andb
---- zenon-0.8.5/zenon.v.orig	2020-10-23 09:19:07.000000000 -0600
-+++ zenon-0.8.5/zenon.v	2026-03-03 16:33:06.988515450 -0700
-@@ -1,6 +1,6 @@
- (*  Copyright 2004 INRIA  *)
- 
--Require Export Classical.
-+From Stdlib Require Export Classical.
- 
- Lemma zenon_notnot : forall P : Prop,
-   P -> (~ P -> False).

zenon.spec

@@ -1,10 +1,15 @@
+# Coq's plugin architecture requires cmxs files, so:
+ExclusiveArch: %{ocaml_native_compiler}
+
+%ifnarch %{ocaml_native_compiler}
 %global debug_package %{nil}
-%global rocqver 9.2.0
+%endif
+%global coqver  8.18.0
 %global giturl  https://github.com/zenon-prover/zenon
 
 Name:		zenon
 Version:	0.8.5
-Release:	43%{?dist}
+Release:	29%{?dist}
 Summary:	Automated theorem prover for first-order classical logic
 License:	BSD-3-Clause
 URL:		http://zenon-prover.org/
@@ -16,31 +21,25 @@ Source3:	%{name}-tptp-ReadMe
 # Basic documentation (man pages). Submitted upstream 2008-07-25:
 Source4:	%{name}.1
 Source5:	%{name}-format.5
-# Update deprecated usage
-Patch:          %{name}-deprecated.patch
 
-# Rocq's plugin architecture requires cmxs files
-ExclusiveArch:  %{ocaml_native_compiler}
-
-BuildRequires:	coq-core-compat = %{rocqver}
-BuildRequires:	rocq = %{rocqver}
-BuildRequires:	rocq-stdlib
+BuildRequires:	coq = %{coqver}
+BuildRequires:	ghostscript
+BuildRequires:	ImageMagick
 BuildRequires:	make
 BuildRequires:	ocaml
 
-Requires:	rocq%{?_isa} = %{rocqver}
-Requires:	rocq-stdlib%{?_isa}
+Requires:	coq%{?_isa} = %{coqver}
 Requires:	coreutils
 
 %description
-Zenon is an automated theorem prover for first order classical logic with
-equality, based on the tableau method.  Zenon can read input files in TPTP,
-Coq, Focal, and its own Zenon format.  Zenon can directly generate Coq proofs
-(proof scripts or proof terms), which can be reinserted into Coq
-specifications.  Zenon can also be extended.
+Zenon is an automated theorem prover for first order classical logic
+with equality, based on the tableau method.  Zenon can read input files
+in TPTP, Coq, Focal, and its own Zenon format.  Zenon can directly
+generate Coq proofs (proof scripts or proof terms), which can be
+reinserted into Coq specifications.  Zenon can also be extended.
 
 %prep
-%autosetup -p1
+%autosetup
 
 cp -p %{SOURCE1} .
 
@@ -54,8 +53,14 @@ mkdir examples
 cp -p %{SOURCE2} examples/tptp-COM003+2.p
 cp -p %{SOURCE3} examples/tptp-ReadMe
 
-make %{?_smp_mflags} zenon.bin
-cp -p zenon.bin zenon
+# Work around Makefile errors (fails if no ocamlopt, uses _bytecode_ otherwise)
+%ifarch %{ocaml_native_compiler}
+  make %{?_smp_mflags} zenon.bin
+  cp -p zenon.bin zenon
+%else
+  make %{?_smp_mflags} zenon.byt
+  cp -p zenon.byt zenon
+%endif
 # Use of %%{?_smp_mflags} sometimes leads to build failures
 make coq
 
@@ -92,50 +97,8 @@ fi
 %{_mandir}/man5/zenon-format.5*
 
 %changelog
-* Wed Jul 29 2026 Jerry James <loganjerry@gmail.com> - 0.8.5-43
-- Rebuild to fix rocq dependencies
-
-* Fri Jul 17 2026 Fedora Release Engineering <releng@fedoraproject.org> - 0.8.5-42
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_45_Mass_Rebuild
-
-* Thu Jul 09 2026 Jerry James <loganjerry@gmail.com> - 0.8.5-41
-- OCaml 5.5.0 rebuild
-
-* Thu Apr 16 2026 Jerry James <loganjerry@gmail.com> - 0.8.5-40
-- Rebuild for rocq 9.2.0
-
-* Thu Mar 19 2026 Jerry James <loganjerry@gmail.com> - 0.8.5-39
-- Rebuild for rocq 9.1.1
-
-* Fri Feb 20 2026 Richard W.M. Jones <rjones@redhat.com> - 0.8.5-38
-- OCaml 5.4.1 rebuild
-
-* Sat Jan 17 2026 Fedora Release Engineering <releng@fedoraproject.org> - 0.8.5-37
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_44_Mass_Rebuild
-
-* Tue Oct 14 2025 Richard W.M. Jones <rjones@redhat.com> - 0.8.5-36
-- OCaml 5.4.0 rebuild
-
-* Fri Aug 22 2025 Jerry James <loganjerry@gmail.com> - 0.8.5-35
-- Bump and rebuild
-
-* Sun Aug 10 2025 Jerry James <loganjerry@gmail.com> - 0.8.5-34
-- Bump and rebuild
-
-* Fri Jul 25 2025 Fedora Release Engineering <releng@fedoraproject.org> - 0.8.5-33
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_43_Mass_Rebuild
-
-* Sat Jul 12 2025 Jerry James <loganjerry@gmail.com> - 0.8.5-32
-- Rebuild to fix OCaml dependencies
-
-* Wed Jan 22 2025 Jerry James <loganjerry@gmail.com> - 0.8.5-31
-- Rebuild for coq 8.20.1
-
-* Sun Jan 19 2025 Fedora Release Engineering <releng@fedoraproject.org> - 0.8.5-30
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_42_Mass_Rebuild
-
-* Fri Jan 10 2025 Jerry James <loganjerry@gmail.com> - 0.8.5-29
-- OCaml 5.3.0 rebuild for Fedora 42
+* Wed Jan 29 2025 Jerry James <loganjerry@gmail.com> - 0.8.5-29
+- OCaml 5.2.1 rebuild for Fedora 41
 
 * Sat Jul 20 2024 Fedora Release Engineering <releng@fedoraproject.org> - 0.8.5-28
 - Rebuilt for https://fedoraproject.org/wiki/Fedora_41_Mass_Rebuild