From 92b3b38506980ea314f0dde852312397d678cd96 Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Sun, 19 Jun 2022 11:40:24 +0100 Subject: [PATCH 01/45] OCaml 4.14.0 rebuild --- zenon.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/zenon.spec b/zenon.spec index a6c07fd..c82dbe8 100644 --- a/zenon.spec +++ b/zenon.spec @@ -7,7 +7,7 @@ Name: zenon Version: 0.8.5 -Release: 6%{?dist} +Release: 7%{?dist} Summary: Automated theorem prover for first-order classical logic License: BSD URL: http://zenon-prover.org/ @@ -94,6 +94,9 @@ fi %{_mandir}/man5/* %changelog +* Sun Jun 19 2022 Richard W.M. Jones - 0.8.5-7 +- OCaml 4.14.0 rebuild + * Fri Mar 25 2022 Jerry James - 0.8.5-6 - Rebuild for coq 8.15.1 From a3b562b1d2b76ec5d1a65a704f13653f8afa1304 Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Sun, 19 Jun 2022 18:27:22 +0100 Subject: [PATCH 02/45] Update coq version to 8.15.2 --- zenon.spec | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/zenon.spec b/zenon.spec index c82dbe8..52a1fb2 100644 --- a/zenon.spec +++ b/zenon.spec @@ -3,7 +3,7 @@ %ifnarch %{ocaml_native_compiler} %global debug_package %{nil} %endif -%global coqver 8.15.1 +%global coqver 8.15.2 Name: zenon Version: 0.8.5 From e297811a571689d61e76a0bf9e847b7a02f67e6a Mon Sep 17 00:00:00 2001 From: Jerry James Date: Tue, 19 Jul 2022 18:20:25 -0600 Subject: [PATCH 03/45] Remove i686 support. --- zenon.spec | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/zenon.spec b/zenon.spec index 52a1fb2..cfcb3fa 100644 --- a/zenon.spec +++ b/zenon.spec @@ -19,6 +19,10 @@ Source3: %{name}-tptp-ReadMe Source4: %{name}.1 Source5: %{name}-format.5 +# ANTLR is unavailable on i686, so coq is also unavailable +# See https://fedoraproject.org/wiki/Changes/Drop_i686_JDKs +ExclusiveArch: %{java_arches} + BuildRequires: coq = %{coqver} BuildRequires: ghostscript BuildRequires: ImageMagick @@ -94,6 +98,9 @@ fi %{_mandir}/man5/* %changelog +* Wed Jul 20 2022 Jerry James - 0.8.5-7 +- Remove i686 support + * Sun Jun 19 2022 Richard W.M. Jones - 0.8.5-7 - OCaml 4.14.0 rebuild From 63d0ec4ac169655f775c2ae472be042e90e86f3b Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Sat, 23 Jul 2022 13:53:34 +0000 Subject: [PATCH 04/45] Rebuilt for https://fedoraproject.org/wiki/Fedora_37_Mass_Rebuild Signed-off-by: Fedora Release Engineering --- zenon.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/zenon.spec b/zenon.spec index cfcb3fa..b242b9a 100644 --- a/zenon.spec +++ b/zenon.spec @@ -7,7 +7,7 @@ Name: zenon Version: 0.8.5 -Release: 7%{?dist} +Release: 8%{?dist} Summary: Automated theorem prover for first-order classical logic License: BSD URL: http://zenon-prover.org/ @@ -98,6 +98,9 @@ fi %{_mandir}/man5/* %changelog +* Sat Jul 23 2022 Fedora Release Engineering - 0.8.5-8 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_37_Mass_Rebuild + * Wed Jul 20 2022 Jerry James - 0.8.5-7 - Remove i686 support From 1afb2f771b64e6b493fe2377abd5f34a13f2127a Mon Sep 17 00:00:00 2001 From: Jerry James Date: Thu, 18 Aug 2022 09:37:46 -0600 Subject: [PATCH 05/45] Rebuild to fix coq dependency. Convert License tag to SPDX. --- zenon.spec | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/zenon.spec b/zenon.spec index b242b9a..432405a 100644 --- a/zenon.spec +++ b/zenon.spec @@ -7,9 +7,9 @@ Name: zenon Version: 0.8.5 -Release: 8%{?dist} +Release: 9%{?dist} Summary: Automated theorem prover for first-order classical logic -License: BSD +License: BSD-3-Clause URL: http://zenon-prover.org/ Source0: https://github.com/zenon-prover/%{name}/archive/%{version}/%{name}-%{version}.tar.gz Source1: http://zenon-prover.org/zenlpar07.pdf @@ -98,6 +98,10 @@ fi %{_mandir}/man5/* %changelog +* Thu Aug 18 2022 Jerry James - 0.8.5-9 +- Rebuild to fix coq dependency +- Convert License tag to SPDX + * Sat Jul 23 2022 Fedora Release Engineering - 0.8.5-8 - Rebuilt for https://fedoraproject.org/wiki/Fedora_37_Mass_Rebuild From 55a46f7b3c2126ac57991b09c854992cff1e0779 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Fri, 16 Sep 2022 14:44:18 -0600 Subject: [PATCH 06/45] Rebuild for coq 8.16.0. --- zenon.spec | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/zenon.spec b/zenon.spec index 432405a..7eb1e39 100644 --- a/zenon.spec +++ b/zenon.spec @@ -3,11 +3,11 @@ %ifnarch %{ocaml_native_compiler} %global debug_package %{nil} %endif -%global coqver 8.15.2 +%global coqver 8.16.0 Name: zenon Version: 0.8.5 -Release: 9%{?dist} +Release: 10%{?dist} Summary: Automated theorem prover for first-order classical logic License: BSD-3-Clause URL: http://zenon-prover.org/ @@ -98,6 +98,9 @@ fi %{_mandir}/man5/* %changelog +* Fri Sep 16 2022 Jerry James - 0.8.5-10 +- Rebuild for coq 8.16.0 + * Thu Aug 18 2022 Jerry James - 0.8.5-9 - Rebuild to fix coq dependency - Convert License tag to SPDX From 84a2c3338cb566ce897278208ba4cbf96fcb68b1 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Sat, 26 Nov 2022 18:25:07 -0700 Subject: [PATCH 07/45] Rebuild for coq 8.16.1. --- zenon.spec | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/zenon.spec b/zenon.spec index 7eb1e39..b52587a 100644 --- a/zenon.spec +++ b/zenon.spec @@ -3,15 +3,15 @@ %ifnarch %{ocaml_native_compiler} %global debug_package %{nil} %endif -%global coqver 8.16.0 +%global coqver 8.16.1 Name: zenon Version: 0.8.5 -Release: 10%{?dist} +Release: 11%{?dist} Summary: Automated theorem prover for first-order classical logic License: BSD-3-Clause URL: http://zenon-prover.org/ -Source0: https://github.com/zenon-prover/%{name}/archive/%{version}/%{name}-%{version}.tar.gz +Source0: https://github.com/zenon-prover/zenon/archive/%{version}/%{name}-%{version}.tar.gz Source1: http://zenon-prover.org/zenlpar07.pdf Source2: %{name}-tptp-COM003+2.p Source3: %{name}-tptp-ReadMe @@ -94,10 +94,13 @@ fi %license LICENSE %{_bindir}/%{name} %{_libdir}/coq/user-contrib/Zenon -%{_mandir}/man1/* -%{_mandir}/man5/* +%{_mandir}/man1/zenon.1* +%{_mandir}/man5/zenon-format.5* %changelog +* Sat Nov 26 2022 Jerry James - 0.8.5-11 +- Rebuild for coq 8.16.1 + * Fri Sep 16 2022 Jerry James - 0.8.5-10 - Rebuild for coq 8.16.0 From 1bd08109812009cb8ec477450b499bb9df6361ac Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Sat, 21 Jan 2023 08:14:09 +0000 Subject: [PATCH 08/45] Rebuilt for https://fedoraproject.org/wiki/Fedora_38_Mass_Rebuild Signed-off-by: Fedora Release Engineering --- zenon.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/zenon.spec b/zenon.spec index b52587a..3afb186 100644 --- a/zenon.spec +++ b/zenon.spec @@ -7,7 +7,7 @@ Name: zenon Version: 0.8.5 -Release: 11%{?dist} +Release: 12%{?dist} Summary: Automated theorem prover for first-order classical logic License: BSD-3-Clause URL: http://zenon-prover.org/ @@ -98,6 +98,9 @@ fi %{_mandir}/man5/zenon-format.5* %changelog +* Sat Jan 21 2023 Fedora Release Engineering - 0.8.5-12 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_38_Mass_Rebuild + * Sat Nov 26 2022 Jerry James - 0.8.5-11 - Rebuild for coq 8.16.1 From 390c2385d6e8e1d8c9f9b3b85e01bef6e6fb785e Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Tue, 24 Jan 2023 16:39:07 +0000 Subject: [PATCH 09/45] Rebuild OCaml packages for F38 --- zenon.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/zenon.spec b/zenon.spec index 3afb186..c818465 100644 --- a/zenon.spec +++ b/zenon.spec @@ -7,7 +7,7 @@ Name: zenon Version: 0.8.5 -Release: 12%{?dist} +Release: 13%{?dist} Summary: Automated theorem prover for first-order classical logic License: BSD-3-Clause URL: http://zenon-prover.org/ @@ -98,6 +98,9 @@ fi %{_mandir}/man5/zenon-format.5* %changelog +* Tue Jan 24 2023 Richard W.M. Jones - 0.8.5-13 +- Rebuild OCaml packages for F38 + * Sat Jan 21 2023 Fedora Release Engineering - 0.8.5-12 - Rebuilt for https://fedoraproject.org/wiki/Fedora_38_Mass_Rebuild From 5c70bc1fc8eac4045574a3f6573190fc9cd17c44 Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Tue, 24 Jan 2023 17:42:04 +0000 Subject: [PATCH 10/45] Bump release and rebuild --- zenon.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/zenon.spec b/zenon.spec index c818465..13c8a64 100644 --- a/zenon.spec +++ b/zenon.spec @@ -7,7 +7,7 @@ Name: zenon Version: 0.8.5 -Release: 13%{?dist} +Release: 14%{?dist} Summary: Automated theorem prover for first-order classical logic License: BSD-3-Clause URL: http://zenon-prover.org/ @@ -98,6 +98,9 @@ fi %{_mandir}/man5/zenon-format.5* %changelog +* Tue Jan 24 2023 Richard W.M. Jones - 0.8.5-14 +- Bump release and rebuild + * Tue Jan 24 2023 Richard W.M. Jones - 0.8.5-13 - Rebuild OCaml packages for F38 From 77525430095a24068b2a01fffb123d2d63380644 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Sat, 1 Apr 2023 11:13:17 -0600 Subject: [PATCH 11/45] Rebuild for coq 8.17.0 --- zenon.spec | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/zenon.spec b/zenon.spec index 13c8a64..7b64af5 100644 --- a/zenon.spec +++ b/zenon.spec @@ -3,11 +3,11 @@ %ifnarch %{ocaml_native_compiler} %global debug_package %{nil} %endif -%global coqver 8.16.1 +%global coqver 8.17.0 Name: zenon Version: 0.8.5 -Release: 14%{?dist} +Release: 15%{?dist} Summary: Automated theorem prover for first-order classical logic License: BSD-3-Clause URL: http://zenon-prover.org/ @@ -98,6 +98,9 @@ fi %{_mandir}/man5/zenon-format.5* %changelog +* Sat Apr 1 2023 Jerry James - 0.8.5-15 +- Rebuild for coq 8.17.0 + * Tue Jan 24 2023 Richard W.M. Jones - 0.8.5-14 - Bump release and rebuild From ab192c62d7cce39a137e023f80756d3d9e6ae8d2 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Mon, 10 Jul 2023 22:37:44 -0600 Subject: [PATCH 12/45] OCaml 5.0.0 rebuild --- zenon.spec | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/zenon.spec b/zenon.spec index 7b64af5..93a8600 100644 --- a/zenon.spec +++ b/zenon.spec @@ -1,13 +1,11 @@ -%undefine _package_note_flags - %ifnarch %{ocaml_native_compiler} %global debug_package %{nil} %endif -%global coqver 8.17.0 +%global coqver 8.17.1 Name: zenon Version: 0.8.5 -Release: 15%{?dist} +Release: 16%{?dist} Summary: Automated theorem prover for first-order classical logic License: BSD-3-Clause URL: http://zenon-prover.org/ @@ -98,6 +96,9 @@ fi %{_mandir}/man5/zenon-format.5* %changelog +* Mon Jul 10 2023 Jerry James - 0.8.5-16 +- OCaml 5.0.0 rebuild + * Sat Apr 1 2023 Jerry James - 0.8.5-15 - Rebuild for coq 8.17.0 From 561f0e6b79e010e2a9ea8c3bd50a9956fb29ffac Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Tue, 11 Jul 2023 11:36:26 +0100 Subject: [PATCH 13/45] ExcludeArch i686 (https://lists.fedoraproject.org/archives/list/devel@lists.fedoraproject.org/message/SPML7CUBSZNI36NLXGVHEG7DNHU3EWOJ/) --- zenon.spec | 3 +++ 1 file changed, 3 insertions(+) diff --git a/zenon.spec b/zenon.spec index 93a8600..d1b7ae4 100644 --- a/zenon.spec +++ b/zenon.spec @@ -1,3 +1,6 @@ +# OCaml packages not built on i686 since OCaml 5 / Fedora 39. +ExcludeArch: %{ix86} + %ifnarch %{ocaml_native_compiler} %global debug_package %{nil} %endif From 9c7af797f20e3a08b0818ad465a643d737ffc42d Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Wed, 12 Jul 2023 13:59:55 +0100 Subject: [PATCH 14/45] OCaml 5.0 rebuild for Fedora 39 --- zenon.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/zenon.spec b/zenon.spec index d1b7ae4..1bf8ae1 100644 --- a/zenon.spec +++ b/zenon.spec @@ -8,7 +8,7 @@ ExcludeArch: %{ix86} Name: zenon Version: 0.8.5 -Release: 16%{?dist} +Release: 17%{?dist} Summary: Automated theorem prover for first-order classical logic License: BSD-3-Clause URL: http://zenon-prover.org/ @@ -99,6 +99,9 @@ fi %{_mandir}/man5/zenon-format.5* %changelog +* Wed Jul 12 2023 Richard W.M. Jones - 0.8.5-17 +- OCaml 5.0 rebuild for Fedora 39 + * Mon Jul 10 2023 Jerry James - 0.8.5-16 - OCaml 5.0.0 rebuild From a637011ec76d15215b173fc2e1ae211299de3cd7 Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Wed, 12 Jul 2023 17:10:30 +0100 Subject: [PATCH 15/45] Only build coq and friends on architectures with the native compiler --- zenon.spec | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/zenon.spec b/zenon.spec index 1bf8ae1..c28d2d2 100644 --- a/zenon.spec +++ b/zenon.spec @@ -1,5 +1,5 @@ -# OCaml packages not built on i686 since OCaml 5 / Fedora 39. -ExcludeArch: %{ix86} +# Coq's plugin architecture requires cmxs files, so: +ExclusiveArch: %{ocaml_native_compiler} %ifnarch %{ocaml_native_compiler} %global debug_package %{nil} From e7453e73da1a987550ac20d53fa783c7d39a71d9 Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Wed, 12 Jul 2023 19:24:41 +0100 Subject: [PATCH 16/45] Comment out duplicate ExclusiveArch --- zenon.spec | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/zenon.spec b/zenon.spec index c28d2d2..a78a6eb 100644 --- a/zenon.spec +++ b/zenon.spec @@ -1,6 +1,10 @@ # Coq's plugin architecture requires cmxs files, so: ExclusiveArch: %{ocaml_native_compiler} +# ANTLR is unavailable on i686, so coq is also unavailable +# See https://fedoraproject.org/wiki/Changes/Drop_i686_JDKs +#ExclusiveArch: %%{java_arches} + %ifnarch %{ocaml_native_compiler} %global debug_package %{nil} %endif @@ -20,10 +24,6 @@ Source3: %{name}-tptp-ReadMe Source4: %{name}.1 Source5: %{name}-format.5 -# ANTLR is unavailable on i686, so coq is also unavailable -# See https://fedoraproject.org/wiki/Changes/Drop_i686_JDKs -ExclusiveArch: %{java_arches} - BuildRequires: coq = %{coqver} BuildRequires: ghostscript BuildRequires: ImageMagick From a2bfad11f3bd886865df015ab7a72589e18409f2 Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Sat, 22 Jul 2023 19:39:29 +0000 Subject: [PATCH 17/45] Rebuilt for https://fedoraproject.org/wiki/Fedora_39_Mass_Rebuild Signed-off-by: Fedora Release Engineering --- zenon.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/zenon.spec b/zenon.spec index a78a6eb..4d02f48 100644 --- a/zenon.spec +++ b/zenon.spec @@ -12,7 +12,7 @@ ExclusiveArch: %{ocaml_native_compiler} Name: zenon Version: 0.8.5 -Release: 17%{?dist} +Release: 18%{?dist} Summary: Automated theorem prover for first-order classical logic License: BSD-3-Clause URL: http://zenon-prover.org/ @@ -99,6 +99,9 @@ fi %{_mandir}/man5/zenon-format.5* %changelog +* Sat Jul 22 2023 Fedora Release Engineering - 0.8.5-18 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_39_Mass_Rebuild + * Wed Jul 12 2023 Richard W.M. Jones - 0.8.5-17 - OCaml 5.0 rebuild for Fedora 39 From 1ab224eb57c96e420c95dc6ed763efbb35446be9 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Thu, 27 Jul 2023 11:17:07 -0600 Subject: [PATCH 18/45] Rebuild for ocaml-zarith 1.13 --- zenon.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/zenon.spec b/zenon.spec index 4d02f48..858627b 100644 --- a/zenon.spec +++ b/zenon.spec @@ -12,7 +12,7 @@ ExclusiveArch: %{ocaml_native_compiler} Name: zenon Version: 0.8.5 -Release: 18%{?dist} +Release: 19%{?dist} Summary: Automated theorem prover for first-order classical logic License: BSD-3-Clause URL: http://zenon-prover.org/ @@ -99,6 +99,9 @@ fi %{_mandir}/man5/zenon-format.5* %changelog +* Thu Jul 27 2023 Jerry James - 0.8.5-19 +- Rebuild for ocaml-zarith 1.13 + * Sat Jul 22 2023 Fedora Release Engineering - 0.8.5-18 - Rebuilt for https://fedoraproject.org/wiki/Fedora_39_Mass_Rebuild From b6424d419294b1c41213c895f3277aaab36678e6 Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Thu, 5 Oct 2023 16:22:39 +0100 Subject: [PATCH 19/45] OCaml 5.1 rebuild for Fedora 40 --- zenon.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/zenon.spec b/zenon.spec index 858627b..11b8f44 100644 --- a/zenon.spec +++ b/zenon.spec @@ -12,7 +12,7 @@ ExclusiveArch: %{ocaml_native_compiler} Name: zenon Version: 0.8.5 -Release: 19%{?dist} +Release: 20%{?dist} Summary: Automated theorem prover for first-order classical logic License: BSD-3-Clause URL: http://zenon-prover.org/ @@ -99,6 +99,9 @@ fi %{_mandir}/man5/zenon-format.5* %changelog +* Thu Oct 05 2023 Richard W.M. Jones - 0.8.5-20 +- OCaml 5.1 rebuild for Fedora 40 + * Thu Jul 27 2023 Jerry James - 0.8.5-19 - Rebuild for ocaml-zarith 1.13 From 960aa15941428703815898d87d950aab979e2f36 Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Tue, 12 Dec 2023 15:40:57 +0000 Subject: [PATCH 20/45] OCaml 5.1.1 rebuild for Fedora 40 --- zenon.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/zenon.spec b/zenon.spec index 11b8f44..178bc5d 100644 --- a/zenon.spec +++ b/zenon.spec @@ -12,7 +12,7 @@ ExclusiveArch: %{ocaml_native_compiler} Name: zenon Version: 0.8.5 -Release: 20%{?dist} +Release: 21%{?dist} Summary: Automated theorem prover for first-order classical logic License: BSD-3-Clause URL: http://zenon-prover.org/ @@ -99,6 +99,9 @@ fi %{_mandir}/man5/zenon-format.5* %changelog +* Tue Dec 12 2023 Richard W.M. Jones - 0.8.5-21 +- OCaml 5.1.1 rebuild for Fedora 40 + * Thu Oct 05 2023 Richard W.M. Jones - 0.8.5-20 - OCaml 5.1 rebuild for Fedora 40 From f4b2af69e5690530c39337d5386289ac85156bd2 Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Mon, 18 Dec 2023 15:30:14 +0000 Subject: [PATCH 21/45] OCaml 5.1.1 + s390x code gen fix for Fedora 40 --- zenon.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/zenon.spec b/zenon.spec index 178bc5d..7692b66 100644 --- a/zenon.spec +++ b/zenon.spec @@ -12,7 +12,7 @@ ExclusiveArch: %{ocaml_native_compiler} Name: zenon Version: 0.8.5 -Release: 21%{?dist} +Release: 22%{?dist} Summary: Automated theorem prover for first-order classical logic License: BSD-3-Clause URL: http://zenon-prover.org/ @@ -99,6 +99,9 @@ fi %{_mandir}/man5/zenon-format.5* %changelog +* Mon Dec 18 2023 Richard W.M. Jones - 0.8.5-22 +- OCaml 5.1.1 + s390x code gen fix for Fedora 40 + * Tue Dec 12 2023 Richard W.M. Jones - 0.8.5-21 - OCaml 5.1.1 rebuild for Fedora 40 From 05c59effb88c24b80b732fae1b31b2ae5ee59a8d Mon Sep 17 00:00:00 2001 From: Jerry James Date: Tue, 2 Jan 2024 12:12:15 -0700 Subject: [PATCH 22/45] Rebuild for coq 8.18.0 --- zenon.spec | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/zenon.spec b/zenon.spec index 7692b66..425e90e 100644 --- a/zenon.spec +++ b/zenon.spec @@ -8,11 +8,11 @@ ExclusiveArch: %{ocaml_native_compiler} %ifnarch %{ocaml_native_compiler} %global debug_package %{nil} %endif -%global coqver 8.17.1 +%global coqver 8.18.0 Name: zenon Version: 0.8.5 -Release: 22%{?dist} +Release: 23%{?dist} Summary: Automated theorem prover for first-order classical logic License: BSD-3-Clause URL: http://zenon-prover.org/ @@ -99,6 +99,9 @@ fi %{_mandir}/man5/zenon-format.5* %changelog +* Tue Jan 2 2024 Jerry James - 0.8.5-23 +- Rebuild for coq 8.18.0 + * Mon Dec 18 2023 Richard W.M. Jones - 0.8.5-22 - OCaml 5.1.1 + s390x code gen fix for Fedora 40 From c20aee4465da6dcdcef84639137390ede4bce717 Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Sat, 27 Jan 2024 11:04:22 +0000 Subject: [PATCH 23/45] Rebuilt for https://fedoraproject.org/wiki/Fedora_40_Mass_Rebuild --- zenon.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/zenon.spec b/zenon.spec index 425e90e..1db8a59 100644 --- a/zenon.spec +++ b/zenon.spec @@ -12,7 +12,7 @@ ExclusiveArch: %{ocaml_native_compiler} Name: zenon Version: 0.8.5 -Release: 23%{?dist} +Release: 24%{?dist} Summary: Automated theorem prover for first-order classical logic License: BSD-3-Clause URL: http://zenon-prover.org/ @@ -99,6 +99,9 @@ fi %{_mandir}/man5/zenon-format.5* %changelog +* Sat Jan 27 2024 Fedora Release Engineering - 0.8.5-24 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_40_Mass_Rebuild + * Tue Jan 2 2024 Jerry James - 0.8.5-23 - Rebuild for coq 8.18.0 From 7cb80570d215bb6cc612f6f4329d5c89d2312400 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Fri, 2 Feb 2024 16:29:48 -0700 Subject: [PATCH 24/45] Rebuild for rebuilt coq --- zenon.spec | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/zenon.spec b/zenon.spec index 1db8a59..0fb97e5 100644 --- a/zenon.spec +++ b/zenon.spec @@ -1,10 +1,6 @@ # Coq's plugin architecture requires cmxs files, so: ExclusiveArch: %{ocaml_native_compiler} -# ANTLR is unavailable on i686, so coq is also unavailable -# See https://fedoraproject.org/wiki/Changes/Drop_i686_JDKs -#ExclusiveArch: %%{java_arches} - %ifnarch %{ocaml_native_compiler} %global debug_package %{nil} %endif @@ -12,7 +8,7 @@ ExclusiveArch: %{ocaml_native_compiler} Name: zenon Version: 0.8.5 -Release: 24%{?dist} +Release: 25%{?dist} Summary: Automated theorem prover for first-order classical logic License: BSD-3-Clause URL: http://zenon-prover.org/ @@ -99,6 +95,9 @@ fi %{_mandir}/man5/zenon-format.5* %changelog +* Fri Feb 2 2024 Jerry James - 0.8.5-25 +- Rebuild for rebuilt coq + * Sat Jan 27 2024 Fedora Release Engineering - 0.8.5-24 - Rebuilt for https://fedoraproject.org/wiki/Fedora_40_Mass_Rebuild From 070ecc9208a5f6902c33d59bc2e31c636f7ccf19 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Thu, 23 May 2024 12:14:12 -0600 Subject: [PATCH 25/45] Add VCS field --- zenon.spec | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/zenon.spec b/zenon.spec index 0fb97e5..c3bdaea 100644 --- a/zenon.spec +++ b/zenon.spec @@ -12,7 +12,8 @@ Release: 25%{?dist} Summary: Automated theorem prover for first-order classical logic License: BSD-3-Clause URL: http://zenon-prover.org/ -Source0: https://github.com/zenon-prover/zenon/archive/%{version}/%{name}-%{version}.tar.gz +VCS: https://github.com/zenon-prover/zenon +Source0: %{vcs}/archive/%{version}/%{name}-%{version}.tar.gz Source1: http://zenon-prover.org/zenlpar07.pdf Source2: %{name}-tptp-COM003+2.p Source3: %{name}-tptp-ReadMe From 948431df6459b976b8c8220435ddd2eb8bf94965 Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Wed, 29 May 2024 22:47:06 +0100 Subject: [PATCH 26/45] OCaml 5.2.0 for Fedora 41 --- zenon.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/zenon.spec b/zenon.spec index c3bdaea..4ece941 100644 --- a/zenon.spec +++ b/zenon.spec @@ -8,7 +8,7 @@ ExclusiveArch: %{ocaml_native_compiler} Name: zenon Version: 0.8.5 -Release: 25%{?dist} +Release: 26%{?dist} Summary: Automated theorem prover for first-order classical logic License: BSD-3-Clause URL: http://zenon-prover.org/ @@ -96,6 +96,9 @@ fi %{_mandir}/man5/zenon-format.5* %changelog +* Wed May 29 2024 Richard W.M. Jones - 0.8.5-26 +- OCaml 5.2.0 for Fedora 41 + * Fri Feb 2 2024 Jerry James - 0.8.5-25 - Rebuild for rebuilt coq From 8454349e2cd160ebcd7a2299ea4405fa419aea84 Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Wed, 19 Jun 2024 19:12:48 +0100 Subject: [PATCH 27/45] OCaml 5.2.0 ppc64le fix --- zenon.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/zenon.spec b/zenon.spec index 4ece941..4140c63 100644 --- a/zenon.spec +++ b/zenon.spec @@ -8,7 +8,7 @@ ExclusiveArch: %{ocaml_native_compiler} Name: zenon Version: 0.8.5 -Release: 26%{?dist} +Release: 27%{?dist} Summary: Automated theorem prover for first-order classical logic License: BSD-3-Clause URL: http://zenon-prover.org/ @@ -96,6 +96,9 @@ fi %{_mandir}/man5/zenon-format.5* %changelog +* Wed Jun 19 2024 Richard W.M. Jones - 0.8.5-27 +- OCaml 5.2.0 ppc64le fix + * Wed May 29 2024 Richard W.M. Jones - 0.8.5-26 - OCaml 5.2.0 for Fedora 41 From 0e1bdbf94c2104b1fb0596cc90b7580e4b3fdeb3 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Wed, 17 Jul 2024 16:21:12 -0600 Subject: [PATCH 28/45] Fix the VCS field --- zenon.spec | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/zenon.spec b/zenon.spec index 4140c63..557f08d 100644 --- a/zenon.spec +++ b/zenon.spec @@ -4,7 +4,8 @@ ExclusiveArch: %{ocaml_native_compiler} %ifnarch %{ocaml_native_compiler} %global debug_package %{nil} %endif -%global coqver 8.18.0 +%global coqver 8.18.0 +%global giturl https://github.com/zenon-prover/zenon Name: zenon Version: 0.8.5 @@ -12,8 +13,8 @@ Release: 27%{?dist} Summary: Automated theorem prover for first-order classical logic License: BSD-3-Clause URL: http://zenon-prover.org/ -VCS: https://github.com/zenon-prover/zenon -Source0: %{vcs}/archive/%{version}/%{name}-%{version}.tar.gz +VCS: git:%{giturl}.git +Source0: %{giturl}/archive/%{version}/%{name}-%{version}.tar.gz Source1: http://zenon-prover.org/zenlpar07.pdf Source2: %{name}-tptp-COM003+2.p Source3: %{name}-tptp-ReadMe From fcec17e073b5a352f6beae2a58e3b4eca742c3a4 Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Sat, 20 Jul 2024 10:50:29 +0000 Subject: [PATCH 29/45] Rebuilt for https://fedoraproject.org/wiki/Fedora_41_Mass_Rebuild --- zenon.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/zenon.spec b/zenon.spec index 557f08d..3b8cb01 100644 --- a/zenon.spec +++ b/zenon.spec @@ -9,7 +9,7 @@ ExclusiveArch: %{ocaml_native_compiler} Name: zenon Version: 0.8.5 -Release: 27%{?dist} +Release: 28%{?dist} Summary: Automated theorem prover for first-order classical logic License: BSD-3-Clause URL: http://zenon-prover.org/ @@ -97,6 +97,9 @@ fi %{_mandir}/man5/zenon-format.5* %changelog +* Sat Jul 20 2024 Fedora Release Engineering - 0.8.5-28 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_41_Mass_Rebuild + * Wed Jun 19 2024 Richard W.M. Jones - 0.8.5-27 - OCaml 5.2.0 ppc64le fix From 6033d8718cd3817ba26a79b6827d4b7a4bb29875 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Fri, 10 Jan 2025 09:44:49 -0700 Subject: [PATCH 30/45] OCaml 5.3.0 rebuild for Fedora 42 --- zenon.spec | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/zenon.spec b/zenon.spec index 3b8cb01..1a7a205 100644 --- a/zenon.spec +++ b/zenon.spec @@ -4,12 +4,12 @@ ExclusiveArch: %{ocaml_native_compiler} %ifnarch %{ocaml_native_compiler} %global debug_package %{nil} %endif -%global coqver 8.18.0 +%global coqver 8.20.0 %global giturl https://github.com/zenon-prover/zenon Name: zenon Version: 0.8.5 -Release: 28%{?dist} +Release: 29%{?dist} Summary: Automated theorem prover for first-order classical logic License: BSD-3-Clause URL: http://zenon-prover.org/ @@ -97,6 +97,9 @@ fi %{_mandir}/man5/zenon-format.5* %changelog +* Fri Jan 10 2025 Jerry James - 0.8.5-29 +- OCaml 5.3.0 rebuild for Fedora 42 + * Sat Jul 20 2024 Fedora Release Engineering - 0.8.5-28 - Rebuilt for https://fedoraproject.org/wiki/Fedora_41_Mass_Rebuild From 673cd36b69afe148d980d454fcac1c0a39f906fc Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Sun, 19 Jan 2025 16:44:12 +0000 Subject: [PATCH 31/45] Rebuilt for https://fedoraproject.org/wiki/Fedora_42_Mass_Rebuild --- zenon.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/zenon.spec b/zenon.spec index 1a7a205..706fd14 100644 --- a/zenon.spec +++ b/zenon.spec @@ -9,7 +9,7 @@ ExclusiveArch: %{ocaml_native_compiler} Name: zenon Version: 0.8.5 -Release: 29%{?dist} +Release: 30%{?dist} Summary: Automated theorem prover for first-order classical logic License: BSD-3-Clause URL: http://zenon-prover.org/ @@ -97,6 +97,9 @@ fi %{_mandir}/man5/zenon-format.5* %changelog +* Sun Jan 19 2025 Fedora Release Engineering - 0.8.5-30 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_42_Mass_Rebuild + * Fri Jan 10 2025 Jerry James - 0.8.5-29 - OCaml 5.3.0 rebuild for Fedora 42 From b9a87dfa9e6159364e693e4cafcee59ca872feca Mon Sep 17 00:00:00 2001 From: Jerry James Date: Wed, 22 Jan 2025 15:37:14 -0700 Subject: [PATCH 32/45] Rebuild for coq 8.20.1 --- zenon.spec | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/zenon.spec b/zenon.spec index 706fd14..91d2d0d 100644 --- a/zenon.spec +++ b/zenon.spec @@ -4,12 +4,12 @@ ExclusiveArch: %{ocaml_native_compiler} %ifnarch %{ocaml_native_compiler} %global debug_package %{nil} %endif -%global coqver 8.20.0 +%global coqver 8.20.1 %global giturl https://github.com/zenon-prover/zenon Name: zenon Version: 0.8.5 -Release: 30%{?dist} +Release: 31%{?dist} Summary: Automated theorem prover for first-order classical logic License: BSD-3-Clause URL: http://zenon-prover.org/ @@ -97,6 +97,9 @@ fi %{_mandir}/man5/zenon-format.5* %changelog +* Wed Jan 22 2025 Jerry James - 0.8.5-31 +- Rebuild for coq 8.20.1 + * Sun Jan 19 2025 Fedora Release Engineering - 0.8.5-30 - Rebuilt for https://fedoraproject.org/wiki/Fedora_42_Mass_Rebuild From 96afada8f4780d41e525951a32e29a7f271ea560 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Sat, 12 Jul 2025 15:21:01 -0600 Subject: [PATCH 33/45] Rebuild to fix OCaml dependencies --- zenon.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/zenon.spec b/zenon.spec index 91d2d0d..83e7992 100644 --- a/zenon.spec +++ b/zenon.spec @@ -9,7 +9,7 @@ ExclusiveArch: %{ocaml_native_compiler} Name: zenon Version: 0.8.5 -Release: 31%{?dist} +Release: 32%{?dist} Summary: Automated theorem prover for first-order classical logic License: BSD-3-Clause URL: http://zenon-prover.org/ @@ -97,6 +97,9 @@ fi %{_mandir}/man5/zenon-format.5* %changelog +* Sat Jul 12 2025 Jerry James - 0.8.5-32 +- Rebuild to fix OCaml dependencies + * Wed Jan 22 2025 Jerry James - 0.8.5-31 - Rebuild for coq 8.20.1 From 1eb3c4026c09b33262dae7febebce4a41bcc8834 Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Fri, 25 Jul 2025 21:17:24 +0000 Subject: [PATCH 34/45] Rebuilt for https://fedoraproject.org/wiki/Fedora_43_Mass_Rebuild --- zenon.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/zenon.spec b/zenon.spec index 83e7992..0d5e5e8 100644 --- a/zenon.spec +++ b/zenon.spec @@ -9,7 +9,7 @@ ExclusiveArch: %{ocaml_native_compiler} Name: zenon Version: 0.8.5 -Release: 32%{?dist} +Release: 33%{?dist} Summary: Automated theorem prover for first-order classical logic License: BSD-3-Clause URL: http://zenon-prover.org/ @@ -97,6 +97,9 @@ fi %{_mandir}/man5/zenon-format.5* %changelog +* Fri Jul 25 2025 Fedora Release Engineering - 0.8.5-33 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_43_Mass_Rebuild + * Sat Jul 12 2025 Jerry James - 0.8.5-32 - Rebuild to fix OCaml dependencies From aa00da82f4b37d6daa99fcac2bdfb1bfcecf9e9f Mon Sep 17 00:00:00 2001 From: Jerry James Date: Sun, 10 Aug 2025 10:42:50 -0600 Subject: [PATCH 35/45] Bump and rebuild --- zenon.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/zenon.spec b/zenon.spec index 0d5e5e8..a246989 100644 --- a/zenon.spec +++ b/zenon.spec @@ -9,7 +9,7 @@ ExclusiveArch: %{ocaml_native_compiler} Name: zenon Version: 0.8.5 -Release: 33%{?dist} +Release: 34%{?dist} Summary: Automated theorem prover for first-order classical logic License: BSD-3-Clause URL: http://zenon-prover.org/ @@ -97,6 +97,9 @@ fi %{_mandir}/man5/zenon-format.5* %changelog +* Sun Aug 10 2025 Jerry James - 0.8.5-34 +- Bump and rebuild + * Fri Jul 25 2025 Fedora Release Engineering - 0.8.5-33 - Rebuilt for https://fedoraproject.org/wiki/Fedora_43_Mass_Rebuild From fe5842f5b32755fde54c1bcedb012b62b3c8170a Mon Sep 17 00:00:00 2001 From: Jerry James Date: Fri, 22 Aug 2025 09:47:09 -0600 Subject: [PATCH 36/45] Bump and rebuild --- zenon.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/zenon.spec b/zenon.spec index a246989..8b09831 100644 --- a/zenon.spec +++ b/zenon.spec @@ -9,7 +9,7 @@ ExclusiveArch: %{ocaml_native_compiler} Name: zenon Version: 0.8.5 -Release: 34%{?dist} +Release: 35%{?dist} Summary: Automated theorem prover for first-order classical logic License: BSD-3-Clause URL: http://zenon-prover.org/ @@ -97,6 +97,9 @@ fi %{_mandir}/man5/zenon-format.5* %changelog +* Fri Aug 22 2025 Jerry James - 0.8.5-35 +- Bump and rebuild + * Sun Aug 10 2025 Jerry James - 0.8.5-34 - Bump and rebuild From d38321127a7821a1128a3a809c5342671092e9aa Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Tue, 14 Oct 2025 09:53:32 +0100 Subject: [PATCH 37/45] OCaml 5.4.0 rebuild --- zenon.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/zenon.spec b/zenon.spec index 8b09831..9c1e0cd 100644 --- a/zenon.spec +++ b/zenon.spec @@ -9,7 +9,7 @@ ExclusiveArch: %{ocaml_native_compiler} Name: zenon Version: 0.8.5 -Release: 35%{?dist} +Release: 36%{?dist} Summary: Automated theorem prover for first-order classical logic License: BSD-3-Clause URL: http://zenon-prover.org/ @@ -97,6 +97,9 @@ fi %{_mandir}/man5/zenon-format.5* %changelog +* Tue Oct 14 2025 Richard W.M. Jones - 0.8.5-36 +- OCaml 5.4.0 rebuild + * Fri Aug 22 2025 Jerry James - 0.8.5-35 - Bump and rebuild From 79034fa8b3e670b59e1309382cc5a54c628eb835 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Wed, 14 Jan 2026 08:54:02 -0700 Subject: [PATCH 38/45] Reflow the description text - Fix a changelog entry --- zenon.spec | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/zenon.spec b/zenon.spec index 9c1e0cd..a2b0723 100644 --- a/zenon.spec +++ b/zenon.spec @@ -32,11 +32,11 @@ 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 @@ -109,7 +109,7 @@ fi * Fri Jul 25 2025 Fedora Release Engineering - 0.8.5-33 - Rebuilt for https://fedoraproject.org/wiki/Fedora_43_Mass_Rebuild -* Sat Jul 12 2025 Jerry James - 0.8.5-32 +* Sat Jul 12 2025 Jerry James - 0.8.5-32 - Rebuild to fix OCaml dependencies * Wed Jan 22 2025 Jerry James - 0.8.5-31 From 67507a4ddf9169d5a88b456ee9e4d184e6ae2c74 Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Sat, 17 Jan 2026 21:07:24 +0000 Subject: [PATCH 39/45] Rebuilt for https://fedoraproject.org/wiki/Fedora_44_Mass_Rebuild --- zenon.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/zenon.spec b/zenon.spec index a2b0723..daad8b2 100644 --- a/zenon.spec +++ b/zenon.spec @@ -9,7 +9,7 @@ ExclusiveArch: %{ocaml_native_compiler} Name: zenon Version: 0.8.5 -Release: 36%{?dist} +Release: 37%{?dist} Summary: Automated theorem prover for first-order classical logic License: BSD-3-Clause URL: http://zenon-prover.org/ @@ -97,6 +97,9 @@ fi %{_mandir}/man5/zenon-format.5* %changelog +* Sat Jan 17 2026 Fedora Release Engineering - 0.8.5-37 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_44_Mass_Rebuild + * Tue Oct 14 2025 Richard W.M. Jones - 0.8.5-36 - OCaml 5.4.0 rebuild From 47d0c43b0f58ae1202829d36250bb35fc45c1852 Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Fri, 20 Feb 2026 23:46:15 +0000 Subject: [PATCH 40/45] OCaml 5.4.1 rebuild --- zenon.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/zenon.spec b/zenon.spec index daad8b2..d3078a0 100644 --- a/zenon.spec +++ b/zenon.spec @@ -9,7 +9,7 @@ ExclusiveArch: %{ocaml_native_compiler} Name: zenon Version: 0.8.5 -Release: 37%{?dist} +Release: 38%{?dist} Summary: Automated theorem prover for first-order classical logic License: BSD-3-Clause URL: http://zenon-prover.org/ @@ -97,6 +97,9 @@ fi %{_mandir}/man5/zenon-format.5* %changelog +* Fri Feb 20 2026 Richard W.M. Jones - 0.8.5-38 +- OCaml 5.4.1 rebuild + * Sat Jan 17 2026 Fedora Release Engineering - 0.8.5-37 - Rebuilt for https://fedoraproject.org/wiki/Fedora_44_Mass_Rebuild From bb037f14a5da8d32452f8625afe48da35f8246b8 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Thu, 19 Mar 2026 21:25:57 -0600 Subject: [PATCH 41/45] Rebuild for rocq 9.1.1 - Add patch to avoid deprecated usage --- zenon-deprecated.patch | 34 ++++++++++++++++++++++++++++++++++ zenon.spec | 36 ++++++++++++++++++------------------ 2 files changed, 52 insertions(+), 18 deletions(-) create mode 100644 zenon-deprecated.patch diff --git a/zenon-deprecated.patch b/zenon-deprecated.patch new file mode 100644 index 0000000..a4bf9fa --- /dev/null +++ b/zenon-deprecated.patch @@ -0,0 +1,34 @@ +--- 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). diff --git a/zenon.spec b/zenon.spec index d3078a0..7f8da93 100644 --- a/zenon.spec +++ b/zenon.spec @@ -1,15 +1,10 @@ -# Coq's plugin architecture requires cmxs files, so: -ExclusiveArch: %{ocaml_native_compiler} - -%ifnarch %{ocaml_native_compiler} %global debug_package %{nil} -%endif -%global coqver 8.20.1 +%global rocqver 9.1.1 %global giturl https://github.com/zenon-prover/zenon Name: zenon Version: 0.8.5 -Release: 38%{?dist} +Release: 39%{?dist} Summary: Automated theorem prover for first-order classical logic License: BSD-3-Clause URL: http://zenon-prover.org/ @@ -21,14 +16,22 @@ 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 -BuildRequires: coq = %{coqver} +# Rocq's plugin architecture requires cmxs files +ExclusiveArch: %{ocaml_native_compiler} + +BuildRequires: coq-core-compat = %{rocqver} +BuildRequires: rocq = %{rocqver} +BuildRequires: rocq-stdlib BuildRequires: ghostscript BuildRequires: ImageMagick BuildRequires: make BuildRequires: ocaml -Requires: coq%{?_isa} = %{coqver} +Requires: rocq%{?_isa} = %{rocqver} +Requires: rocq-stdlib%{?_isa} Requires: coreutils %description @@ -39,7 +42,7 @@ Coq, Focal, and its own Zenon format. Zenon can directly generate Coq proofs specifications. Zenon can also be extended. %prep -%autosetup +%autosetup -p1 cp -p %{SOURCE1} . @@ -53,14 +56,8 @@ mkdir examples cp -p %{SOURCE2} examples/tptp-COM003+2.p cp -p %{SOURCE3} examples/tptp-ReadMe -# 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 +make %{?_smp_mflags} zenon.bin +cp -p zenon.bin zenon # Use of %%{?_smp_mflags} sometimes leads to build failures make coq @@ -97,6 +94,9 @@ fi %{_mandir}/man5/zenon-format.5* %changelog +* Thu Mar 19 2026 Jerry James - 0.8.5-39 +- Rebuild for rocq 9.1.1 + * Fri Feb 20 2026 Richard W.M. Jones - 0.8.5-38 - OCaml 5.4.1 rebuild From 908bb57416601be25a1d13ea5ce7b173c14d12bf Mon Sep 17 00:00:00 2001 From: Jerry James Date: Thu, 16 Apr 2026 11:36:07 -0600 Subject: [PATCH 42/45] Rebuild for rocq 9.2.0 --- zenon.spec | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/zenon.spec b/zenon.spec index 7f8da93..4080b82 100644 --- a/zenon.spec +++ b/zenon.spec @@ -1,10 +1,10 @@ %global debug_package %{nil} -%global rocqver 9.1.1 +%global rocqver 9.2.0 %global giturl https://github.com/zenon-prover/zenon Name: zenon Version: 0.8.5 -Release: 39%{?dist} +Release: 40%{?dist} Summary: Automated theorem prover for first-order classical logic License: BSD-3-Clause URL: http://zenon-prover.org/ @@ -94,6 +94,9 @@ fi %{_mandir}/man5/zenon-format.5* %changelog +* Thu Apr 16 2026 Jerry James - 0.8.5-40 +- Rebuild for rocq 9.2.0 + * Thu Mar 19 2026 Jerry James - 0.8.5-39 - Rebuild for rocq 9.1.1 From 690b763b983f1a9ec4252d659fefa13539182a96 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Thu, 9 Jul 2026 16:29:13 -0600 Subject: [PATCH 43/45] OCaml 5.5.0 rebuild --- zenon.spec | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/zenon.spec b/zenon.spec index 4080b82..0e57e4d 100644 --- a/zenon.spec +++ b/zenon.spec @@ -4,7 +4,7 @@ Name: zenon Version: 0.8.5 -Release: 40%{?dist} +Release: 41%{?dist} Summary: Automated theorem prover for first-order classical logic License: BSD-3-Clause URL: http://zenon-prover.org/ @@ -25,8 +25,6 @@ ExclusiveArch: %{ocaml_native_compiler} BuildRequires: coq-core-compat = %{rocqver} BuildRequires: rocq = %{rocqver} BuildRequires: rocq-stdlib -BuildRequires: ghostscript -BuildRequires: ImageMagick BuildRequires: make BuildRequires: ocaml @@ -94,6 +92,9 @@ fi %{_mandir}/man5/zenon-format.5* %changelog +* Thu Jul 09 2026 Jerry James - 0.8.5-41 +- OCaml 5.5.0 rebuild + * Thu Apr 16 2026 Jerry James - 0.8.5-40 - Rebuild for rocq 9.2.0 From d706603ef8efc78e7c4db8b6a8d0a621eea92adb Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Fri, 17 Jul 2026 09:39:45 +0000 Subject: [PATCH 44/45] Rebuilt for https://fedoraproject.org/wiki/Fedora_45_Mass_Rebuild --- zenon.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/zenon.spec b/zenon.spec index 0e57e4d..7f5fe8b 100644 --- a/zenon.spec +++ b/zenon.spec @@ -4,7 +4,7 @@ Name: zenon Version: 0.8.5 -Release: 41%{?dist} +Release: 42%{?dist} Summary: Automated theorem prover for first-order classical logic License: BSD-3-Clause URL: http://zenon-prover.org/ @@ -92,6 +92,9 @@ fi %{_mandir}/man5/zenon-format.5* %changelog +* Fri Jul 17 2026 Fedora Release Engineering - 0.8.5-42 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_45_Mass_Rebuild + * Thu Jul 09 2026 Jerry James - 0.8.5-41 - OCaml 5.5.0 rebuild From 89d4ce2b46abd5ecae0cf7347256acd9ac5c52a9 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Wed, 29 Jul 2026 12:07:50 -0600 Subject: [PATCH 45/45] Rebuild to fix rocq dependencies --- zenon.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/zenon.spec b/zenon.spec index 7f5fe8b..b208d71 100644 --- a/zenon.spec +++ b/zenon.spec @@ -4,7 +4,7 @@ Name: zenon Version: 0.8.5 -Release: 42%{?dist} +Release: 43%{?dist} Summary: Automated theorem prover for first-order classical logic License: BSD-3-Clause URL: http://zenon-prover.org/ @@ -92,6 +92,9 @@ fi %{_mandir}/man5/zenon-format.5* %changelog +* Wed Jul 29 2026 Jerry James - 0.8.5-43 +- Rebuild to fix rocq dependencies + * Fri Jul 17 2026 Fedora Release Engineering - 0.8.5-42 - Rebuilt for https://fedoraproject.org/wiki/Fedora_45_Mass_Rebuild