From 5a5b54780466a11bb8b117c6019beb81c51524fa Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Wed, 2 Sep 2020 23:42:22 +0100 Subject: [PATCH 01/66] Bump release and rebuild. --- zenon.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/zenon.spec b/zenon.spec index b8c04f9..032dd00 100644 --- a/zenon.spec +++ b/zenon.spec @@ -5,7 +5,7 @@ Name: zenon Version: 0.8.4 -Release: 17%{?dist} +Release: 17%{?dist}.1 Summary: Automated theorem prover for first-order classical logic License: BSD URL: http://zenon-prover.org/ @@ -98,6 +98,9 @@ fi %{_mandir}/man5/* %changelog +* Wed Sep 02 2020 Richard W.M. Jones - 0.8.4-17.1 +- Bump release and rebuild. + * Wed Sep 02 2020 Richard W.M. Jones - 0.8.4-17 - OCaml 4.11.1 rebuild From cb45e33f6fb5cfbd69d72c43f59cc973bfc630a1 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Mon, 9 Nov 2020 21:38:54 -0700 Subject: [PATCH 02/66] Explicitly BR make. --- zenon.spec | 1 + 1 file changed, 1 insertion(+) diff --git a/zenon.spec b/zenon.spec index b8c04f9..c87c54c 100644 --- a/zenon.spec +++ b/zenon.spec @@ -27,6 +27,7 @@ ExcludeArch: s390x BuildRequires: coq = %{coqver} BuildRequires: ghostscript-core BuildRequires: ImageMagick +BuildRequires: make BuildRequires: ocaml Requires: coq%{?_isa} = %{coqver} From 9ae522ced151a0b38907ab8fecf5423a8cf5484f Mon Sep 17 00:00:00 2001 From: Jerry James Date: Wed, 2 Dec 2020 16:12:08 -0700 Subject: [PATCH 03/66] Rebuild for coq 8.12.1. --- zenon.spec | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/zenon.spec b/zenon.spec index c87c54c..6bb5354 100644 --- a/zenon.spec +++ b/zenon.spec @@ -1,11 +1,11 @@ %ifnarch %{ocaml_native_compiler} %global debug_package %{nil} %endif -%global coqver 8.12.0 +%global coqver 8.12.1 Name: zenon Version: 0.8.4 -Release: 17%{?dist} +Release: 18%{?dist} Summary: Automated theorem prover for first-order classical logic License: BSD URL: http://zenon-prover.org/ @@ -99,6 +99,9 @@ fi %{_mandir}/man5/* %changelog +* Wed Dec 2 2020 Jerry James - 0.8.4-18 +- Rebuild for coq 8.12.1 + * Wed Sep 02 2020 Richard W.M. Jones - 0.8.4-17 - OCaml 4.11.1 rebuild From 600cf4803673f071bc3c8f8f09397869b5c164ca Mon Sep 17 00:00:00 2001 From: Jerry James Date: Mon, 9 Nov 2020 21:38:54 -0700 Subject: [PATCH 04/66] Explicitly BR make. --- zenon.spec | 1 + 1 file changed, 1 insertion(+) diff --git a/zenon.spec b/zenon.spec index 032dd00..1716efb 100644 --- a/zenon.spec +++ b/zenon.spec @@ -27,6 +27,7 @@ ExcludeArch: s390x BuildRequires: coq = %{coqver} BuildRequires: ghostscript-core BuildRequires: ImageMagick +BuildRequires: make BuildRequires: ocaml Requires: coq%{?_isa} = %{coqver} From 6d1d5c244f9fc7ae0761406ba1259addd2879c52 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Wed, 2 Dec 2020 16:12:08 -0700 Subject: [PATCH 05/66] Rebuild for coq 8.12.1. --- zenon.spec | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/zenon.spec b/zenon.spec index 1716efb..54cdfb2 100644 --- a/zenon.spec +++ b/zenon.spec @@ -1,11 +1,11 @@ %ifnarch %{ocaml_native_compiler} %global debug_package %{nil} %endif -%global coqver 8.12.0 +%global coqver 8.12.1 Name: zenon Version: 0.8.4 -Release: 17%{?dist}.1 +Release: 18%{?dist} Summary: Automated theorem prover for first-order classical logic License: BSD URL: http://zenon-prover.org/ @@ -99,6 +99,9 @@ fi %{_mandir}/man5/* %changelog +* Wed Dec 2 2020 Jerry James - 0.8.4-18 +- Rebuild for coq 8.12.1 + * Wed Sep 02 2020 Richard W.M. Jones - 0.8.4-17.1 - Bump release and rebuild. From 75f6efcd607b9c6d5b7385af62ec0907a4f78d80 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Wed, 23 Dec 2020 20:03:11 -0700 Subject: [PATCH 06/66] Rebuild for coq 8.12.2. --- zenon.spec | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/zenon.spec b/zenon.spec index 6bb5354..af43442 100644 --- a/zenon.spec +++ b/zenon.spec @@ -1,11 +1,11 @@ %ifnarch %{ocaml_native_compiler} %global debug_package %{nil} %endif -%global coqver 8.12.1 +%global coqver 8.12.2 Name: zenon Version: 0.8.4 -Release: 18%{?dist} +Release: 19%{?dist} Summary: Automated theorem prover for first-order classical logic License: BSD URL: http://zenon-prover.org/ @@ -99,6 +99,9 @@ fi %{_mandir}/man5/* %changelog +* Wed Dec 23 2020 Jerry James - 0.8.4-19 +- Rebuild for coq 8.12.2 + * Wed Dec 2 2020 Jerry James - 0.8.4-18 - Rebuild for coq 8.12.1 From db886e0d578fa2793efb01532e1da25252a50aa4 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Wed, 23 Dec 2020 20:03:11 -0700 Subject: [PATCH 07/66] Rebuild for coq 8.12.2. --- zenon.spec | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/zenon.spec b/zenon.spec index 54cdfb2..4cdf784 100644 --- a/zenon.spec +++ b/zenon.spec @@ -1,11 +1,11 @@ %ifnarch %{ocaml_native_compiler} %global debug_package %{nil} %endif -%global coqver 8.12.1 +%global coqver 8.12.2 Name: zenon Version: 0.8.4 -Release: 18%{?dist} +Release: 19%{?dist} Summary: Automated theorem prover for first-order classical logic License: BSD URL: http://zenon-prover.org/ @@ -99,6 +99,9 @@ fi %{_mandir}/man5/* %changelog +* Wed Dec 23 2020 Jerry James - 0.8.4-19 +- Rebuild for coq 8.12.2 + * Wed Dec 2 2020 Jerry James - 0.8.4-18 - Rebuild for coq 8.12.1 From f725979dd55e016c549f12e1ce03ec08c24deb32 Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Thu, 28 Jan 2021 00:40:35 +0000 Subject: [PATCH 08/66] - Rebuilt for https://fedoraproject.org/wiki/Fedora_34_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 af43442..f23936f 100644 --- a/zenon.spec +++ b/zenon.spec @@ -5,7 +5,7 @@ Name: zenon Version: 0.8.4 -Release: 19%{?dist} +Release: 20%{?dist} Summary: Automated theorem prover for first-order classical logic License: BSD URL: http://zenon-prover.org/ @@ -99,6 +99,9 @@ fi %{_mandir}/man5/* %changelog +* Thu Jan 28 2021 Fedora Release Engineering - 0.8.4-20 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_34_Mass_Rebuild + * Wed Dec 23 2020 Jerry James - 0.8.4-19 - Rebuild for coq 8.12.2 From 08ef82895e09cc93f6da2a12ec01cc3fd4090129 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Sat, 20 Feb 2021 23:41:46 -0700 Subject: [PATCH 09/66] Rebuild for coq 8.13.0. --- zenon.spec | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/zenon.spec b/zenon.spec index f23936f..2a627bf 100644 --- a/zenon.spec +++ b/zenon.spec @@ -1,11 +1,11 @@ %ifnarch %{ocaml_native_compiler} %global debug_package %{nil} %endif -%global coqver 8.12.2 +%global coqver 8.13.0 Name: zenon Version: 0.8.4 -Release: 20%{?dist} +Release: 21%{?dist} Summary: Automated theorem prover for first-order classical logic License: BSD URL: http://zenon-prover.org/ @@ -99,6 +99,9 @@ fi %{_mandir}/man5/* %changelog +* Sat Feb 20 2021 Jerry James - 0.8.4-21 +- Rebuild for coq 8.13.0 + * Thu Jan 28 2021 Fedora Release Engineering - 0.8.4-20 - Rebuilt for https://fedoraproject.org/wiki/Fedora_34_Mass_Rebuild From cb886e14101fd1fe7d26fa7e709166122ff52d19 Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Tue, 2 Mar 2021 11:03:38 +0000 Subject: [PATCH 10/66] OCaml 4.12.0 build --- zenon.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/zenon.spec b/zenon.spec index 2a627bf..c71f9f8 100644 --- a/zenon.spec +++ b/zenon.spec @@ -5,7 +5,7 @@ Name: zenon Version: 0.8.4 -Release: 21%{?dist} +Release: 22%{?dist} Summary: Automated theorem prover for first-order classical logic License: BSD URL: http://zenon-prover.org/ @@ -99,6 +99,9 @@ fi %{_mandir}/man5/* %changelog +* Tue Mar 2 11:03:37 GMT 2021 Richard W.M. Jones - 0.8.4-22 +- OCaml 4.12.0 build + * Sat Feb 20 2021 Jerry James - 0.8.4-21 - Rebuild for coq 8.13.0 From 0fb275fe8cb441c48ef1b6bb6b54ae13cb11be6d Mon Sep 17 00:00:00 2001 From: Jerry James Date: Wed, 3 Mar 2021 13:46:46 -0700 Subject: [PATCH 11/66] Rebuild for coq 8.13.1. --- zenon.spec | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/zenon.spec b/zenon.spec index c71f9f8..98e96e8 100644 --- a/zenon.spec +++ b/zenon.spec @@ -1,11 +1,11 @@ %ifnarch %{ocaml_native_compiler} %global debug_package %{nil} %endif -%global coqver 8.13.0 +%global coqver 8.13.1 Name: zenon Version: 0.8.4 -Release: 22%{?dist} +Release: 23%{?dist} Summary: Automated theorem prover for first-order classical logic License: BSD URL: http://zenon-prover.org/ @@ -99,6 +99,9 @@ fi %{_mandir}/man5/* %changelog +* Wed Mar 3 2021 Jerry James - 0.8.4-23 +- Rebuild for coq 8.13.1 + * Tue Mar 2 11:03:37 GMT 2021 Richard W.M. Jones - 0.8.4-22 - OCaml 4.12.0 build From 76c325bae8a6661c8dfb486f7ce5fc45cb8c0b1c Mon Sep 17 00:00:00 2001 From: Jerry James Date: Sat, 12 Jun 2021 15:18:14 -0600 Subject: [PATCH 12/66] Rebuild for coq 8.13.2. --- zenon.spec | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/zenon.spec b/zenon.spec index 98e96e8..296f3bb 100644 --- a/zenon.spec +++ b/zenon.spec @@ -1,11 +1,11 @@ %ifnarch %{ocaml_native_compiler} %global debug_package %{nil} %endif -%global coqver 8.13.1 +%global coqver 8.13.2 Name: zenon Version: 0.8.4 -Release: 23%{?dist} +Release: 24%{?dist} Summary: Automated theorem prover for first-order classical logic License: BSD URL: http://zenon-prover.org/ @@ -25,7 +25,7 @@ Patch1: %{name}-ocaml.patch ExcludeArch: s390x BuildRequires: coq = %{coqver} -BuildRequires: ghostscript-core +BuildRequires: ghostscript BuildRequires: ImageMagick BuildRequires: make BuildRequires: ocaml @@ -99,6 +99,9 @@ fi %{_mandir}/man5/* %changelog +* Tue Jun 8 2021 Jerry James - 0.8.4-24 +- Rebuild for coq 8.13.2 + * Wed Mar 3 2021 Jerry James - 0.8.4-23 - Rebuild for coq 8.13.1 From e5c4ed1bc3e7d18c2d15893ea4abda4b7d0fb31c Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Fri, 23 Jul 2021 22:16:19 +0000 Subject: [PATCH 13/66] - Rebuilt for https://fedoraproject.org/wiki/Fedora_35_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 296f3bb..58dd9c2 100644 --- a/zenon.spec +++ b/zenon.spec @@ -5,7 +5,7 @@ Name: zenon Version: 0.8.4 -Release: 24%{?dist} +Release: 25%{?dist} Summary: Automated theorem prover for first-order classical logic License: BSD URL: http://zenon-prover.org/ @@ -99,6 +99,9 @@ fi %{_mandir}/man5/* %changelog +* Fri Jul 23 2021 Fedora Release Engineering - 0.8.4-25 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_35_Mass_Rebuild + * Tue Jun 8 2021 Jerry James - 0.8.4-24 - Rebuild for coq 8.13.2 From 0fd21d5256e39ceb726c503f8cc8c4544aa1fc88 Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Mon, 4 Oct 2021 18:23:52 +0100 Subject: [PATCH 14/66] Try to build on s390x with OCaml 4.13 --- zenon.spec | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/zenon.spec b/zenon.spec index 58dd9c2..a221a4c 100644 --- a/zenon.spec +++ b/zenon.spec @@ -5,7 +5,7 @@ Name: zenon Version: 0.8.4 -Release: 25%{?dist} +Release: 26%{?dist} Summary: Automated theorem prover for first-order classical logic License: BSD URL: http://zenon-prover.org/ @@ -21,9 +21,6 @@ Patch0: %{name}-coq89.patch # Adapt to ocaml 4.08 and later Patch1: %{name}-ocaml.patch -# https://bugzilla.redhat.com/show_bug.cgi?id=1874879 -ExcludeArch: s390x - BuildRequires: coq = %{coqver} BuildRequires: ghostscript BuildRequires: ImageMagick @@ -99,6 +96,9 @@ fi %{_mandir}/man5/* %changelog +* Mon Oct 04 2021 Richard W.M. Jones - 0.8.4-26 +- Try to build on s390x with OCaml 4.13 + * Fri Jul 23 2021 Fedora Release Engineering - 0.8.4-25 - Rebuilt for https://fedoraproject.org/wiki/Fedora_35_Mass_Rebuild From 0242d4ce5446fd74450beca972d8aa89d1da8c5c Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Tue, 5 Oct 2021 15:03:26 +0100 Subject: [PATCH 15/66] OCaml 4.13.1 build --- zenon.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/zenon.spec b/zenon.spec index a221a4c..99c4814 100644 --- a/zenon.spec +++ b/zenon.spec @@ -5,7 +5,7 @@ Name: zenon Version: 0.8.4 -Release: 26%{?dist} +Release: 27%{?dist} Summary: Automated theorem prover for first-order classical logic License: BSD URL: http://zenon-prover.org/ @@ -96,6 +96,9 @@ fi %{_mandir}/man5/* %changelog +* Tue Oct 05 2021 Richard W.M. Jones - 0.8.4-27 +- OCaml 4.13.1 build + * Mon Oct 04 2021 Richard W.M. Jones - 0.8.4-26 - Try to build on s390x with OCaml 4.13 From 34ece0b6b3a278b6ec2425e952e78ef5f107041e Mon Sep 17 00:00:00 2001 From: Jerry James Date: Thu, 21 Oct 2021 11:32:51 -0600 Subject: [PATCH 16/66] Version 0.8.5. Drop upstreamed -coq89 and -ocaml patches. --- README.md | 9 +++ sources | 2 +- zenon-coq89.patch | 174 ---------------------------------------------- zenon-ocaml.patch | 55 --------------- zenon.spec | 16 ++--- 5 files changed, 18 insertions(+), 238 deletions(-) create mode 100644 README.md delete mode 100644 zenon-coq89.patch delete mode 100644 zenon-ocaml.patch diff --git a/README.md b/README.md new file mode 100644 index 0000000..92f51c8 --- /dev/null +++ b/README.md @@ -0,0 +1,9 @@ +# zenon + +Zenon is an extensible authomated theorem prover whose main claim to fame is +that it produces actual proofs of theorems. Correctness is an explicit +non-goal in the design of Zenon: the proof output needs to be checked by +another program before the theorem is considered proved. As a consequence, +Zenon is not designed for direct use by humans, but rather for interfacing +into formal proof systems, such as interactive proof assistants and +non-interactive proof checkers. diff --git a/sources b/sources index 1567f91..bf4128f 100644 --- a/sources +++ b/sources @@ -1,2 +1,2 @@ -SHA512 (zenon-0.8.4.tar.gz) = a60ad321e7eedc00390d11ff91f25d64c7a3fe2eafa23a330e345df02a30ca6964a40e4495b7eeb25e19ed9b7f61b65772c3184ff2b2f85b03e63dc481645e91 +SHA512 (zenon-0.8.5.tar.gz) = dc97cc02bcc2e76a1130f4f7e44ba9839126b5e15f4488ac32d47aef330cbb9ea8c2f1b34f8543ed243587e95848a7187c003a300feed0da64ec81f4501b3bdb SHA512 (zenlpar07.pdf) = f8a24ba1c32015ea315946042b39f0b629094553097f43c8fb37041450d39b64e3a781006bdcbae42919104907efec9f0cf065d675f3ff09af891d9d28c2549f diff --git a/zenon-coq89.patch b/zenon-coq89.patch deleted file mode 100644 index 9e28577..0000000 --- a/zenon-coq89.patch +++ /dev/null @@ -1,174 +0,0 @@ ---- zenon_coqbool.v.orig 2018-09-18 09:01:37.000000000 -0600 -+++ zenon_coqbool.v 2019-05-31 09:34:36.433667055 -0600 -@@ -143,7 +143,7 @@ Proof. - intros A B r cond; unfold Is_true; destruct cond; auto. - Qed. - --Implicit Arguments zenon_coqbool_ite_rel_l [A B]. -+Arguments zenon_coqbool_ite_rel_l [A B]. - - Lemma zenon_coqbool_ite_rel_r : - forall (A B : Type) (r: A -> B -> Prop) (e1 : A) (cond : bool) (thn els : B), -@@ -154,7 +154,7 @@ Proof. - intros A B r e1 cond; unfold Is_true; destruct cond; auto. - Qed. - --Implicit Arguments zenon_coqbool_ite_rel_r [A B]. -+Arguments zenon_coqbool_ite_rel_r [A B]. - - Lemma zenon_coqbool_ite_rel_nl : - forall (A B : Type) (r: A -> B -> Prop) (cond : bool) (thn els : A) (e2 : B), -@@ -165,7 +165,7 @@ Proof. - intros A B r cond; unfold Is_true; destruct cond; auto. - Qed. - --Implicit Arguments zenon_coqbool_ite_rel_nl [A B]. -+Arguments zenon_coqbool_ite_rel_nl [A B]. - - Lemma zenon_coqbool_ite_rel_nr : - forall (A B : Type) (r: A -> B -> Prop) (e1 : A) (cond : bool) (thn els : B), -@@ -176,7 +176,7 @@ Proof. - intros A B r e1 cond; unfold Is_true; destruct cond; auto. - Qed. - --Implicit Arguments zenon_coqbool_ite_rel_nr [A B]. -+Arguments zenon_coqbool_ite_rel_nr [A B]. - - (* ************************************************ *) - -@@ -216,19 +216,19 @@ Definition zenon_coqbool_ite_rel_l_s := - fun A B r i t e e2 c h1 h2 - => @zenon_coqbool_ite_rel_l A B r i t e e2 h1 h2 c - . --Implicit Arguments zenon_coqbool_ite_rel_l_s [A B]. -+Arguments zenon_coqbool_ite_rel_l_s [A B]. - Definition zenon_coqbool_ite_rel_r_s := - fun A B r e1 i t e c h1 h2 - => @zenon_coqbool_ite_rel_r A B r e1 i t e h1 h2 c - . --Implicit Arguments zenon_coqbool_ite_rel_r_s [A B]. -+Arguments zenon_coqbool_ite_rel_r_s [A B]. - Definition zenon_coqbool_ite_rel_nl_s := - fun A B r i t e e2 c h1 h2 - => @zenon_coqbool_ite_rel_nl A B r i t e e2 h1 h2 c - . --Implicit Arguments zenon_coqbool_ite_rel_nl_s [A B]. -+Arguments zenon_coqbool_ite_rel_nl_s [A B]. - Definition zenon_coqbool_ite_rel_nr_s := - fun A B r e1 i t e c h1 h2 - => @zenon_coqbool_ite_rel_nr A B r e1 i t e h1 h2 c - . --Implicit Arguments zenon_coqbool_ite_rel_nr_s [A B]. -+Arguments zenon_coqbool_ite_rel_nr_s [A B]. ---- zenon_focal.v.orig 2018-09-18 09:01:37.000000000 -0600 -+++ zenon_focal.v 2019-05-31 09:34:54.814494601 -0600 -@@ -198,7 +198,7 @@ Proof. - intros A B r cond; unfold Is_true; destruct cond; auto. - Qed. - --Implicit Arguments zenon_focal_ite_rel_l [A B]. -+Arguments zenon_focal_ite_rel_l [A B]. - - Lemma zenon_focal_ite_rel_r : - forall (A B : Type) (r: A -> B -> Prop) (e1 : A) (cond : bool) (thn els : B), -@@ -209,7 +209,7 @@ Proof. - intros A B r e1 cond; unfold Is_true; destruct cond; auto. - Qed. - --Implicit Arguments zenon_focal_ite_rel_r [A B]. -+Arguments zenon_focal_ite_rel_r [A B]. - - Lemma zenon_focal_ite_rel_nl : - forall (A B : Type) (r: A -> B -> Prop) (cond : bool) (thn els : A) (e2 : B), -@@ -220,7 +220,7 @@ Proof. - intros A B r cond; unfold Is_true; destruct cond; auto. - Qed. - --Implicit Arguments zenon_focal_ite_rel_nl [A B]. -+Arguments zenon_focal_ite_rel_nl [A B]. - - Lemma zenon_focal_ite_rel_nr : - forall (A B : Type) (r: A -> B -> Prop) (e1 : A) (cond : bool) (thn els : B), -@@ -231,7 +231,7 @@ Proof. - intros A B r e1 cond; unfold Is_true; destruct cond; auto. - Qed. - --Implicit Arguments zenon_focal_ite_rel_nr [A B]. -+Arguments zenon_focal_ite_rel_nr [A B]. - - Lemma zenon_focal_istrue_true : forall e, - (e = true -> False) -> (Is_true e -> False). -@@ -313,19 +313,19 @@ Definition zenon_focal_ite_rel_l_s := - fun A B r i t e e2 c h1 h2 - => @zenon_focal_ite_rel_l A B r i t e e2 h1 h2 c - . --Implicit Arguments zenon_focal_ite_rel_l_s [A B]. -+Arguments zenon_focal_ite_rel_l_s [A B]. - Definition zenon_focal_ite_rel_r_s := - fun A B r e1 i t e c h1 h2 - => @zenon_focal_ite_rel_r A B r e1 i t e h1 h2 c - . --Implicit Arguments zenon_focal_ite_rel_r_s [A B]. -+Arguments zenon_focal_ite_rel_r_s [A B]. - Definition zenon_focal_ite_rel_nl_s := - fun A B r i t e e2 c h1 h2 - => @zenon_focal_ite_rel_nl A B r i t e e2 h1 h2 c - . --Implicit Arguments zenon_focal_ite_rel_nl_s [A B]. -+Arguments zenon_focal_ite_rel_nl_s [A B]. - Definition zenon_focal_ite_rel_nr_s := - fun A B r e1 i t e c h1 h2 - => @zenon_focal_ite_rel_nr A B r e1 i t e h1 h2 c - . --Implicit Arguments zenon_focal_ite_rel_nr_s [A B]. -+Arguments zenon_focal_ite_rel_nr_s [A B]. ---- zenon_induct.v.orig 2018-09-18 09:01:37.000000000 -0600 -+++ zenon_induct.v 2019-05-31 09:39:07.572218768 -0600 -@@ -12,13 +12,13 @@ Lemma zenon_induct_f_equal : forall (T1 - (f x = f y -> False) -> (x = y -> False). - Proof. intros T1 T2 x y f H1 H2. apply H1. subst x. auto. Qed. - --Implicit Arguments zenon_induct_f_equal [T1 T2]. -+Arguments zenon_induct_f_equal [T1 T2]. - - Definition zenon_induct_f_equal_s := - fun t1 t2 x y f c h => @zenon_induct_f_equal t1 t2 x y f h c - . - --Implicit Arguments zenon_induct_f_equal_s [t1 t2]. -+Arguments zenon_induct_f_equal_s [t1 t2]. - - Lemma zenon_induct_case_subs : forall (T : Type) (b a : T) P, - (b = a -> P(a) -> False) -> b = a -> P(b) -> False. ---- zenon.v.orig 2018-09-18 09:01:37.000000000 -0600 -+++ zenon.v 2019-05-31 09:34:15.884859849 -0600 -@@ -71,7 +71,7 @@ Lemma zenon_notallex : forall (T : Type) - Proof. - firstorder. apply H0. intro x. apply NNPP. intro nPx. apply (H x nPx). - Qed. --Implicit Arguments zenon_notallex [T]. -+Arguments zenon_notallex [T]. - - Lemma zenon_subst : - forall (T : Type) (P : T -> Prop) (a b : T), -@@ -111,7 +111,7 @@ Definition zenon_notequiv_s := fun P Q c - Definition zenon_ex_s := fun T P c h => zenon_ex T P h c. - Definition zenon_notall_s := fun T P c h => zenon_notall T P h c. - Definition zenon_notallex_s := fun T P c h => @zenon_notallex T P h c. --Implicit Arguments zenon_notallex_s [T]. -+Arguments zenon_notallex_s [T]. - - Definition zenon_subst_s := fun T P x y c h i => zenon_subst T P x y h i c. - Definition zenon_pnotp_s := fun P Q c h i => zenon_pnotp P Q h i c. -@@ -142,9 +142,9 @@ Proof. - auto. - Qed. - --Implicit Arguments zenon_recfun_unfold [A]. -+Arguments zenon_recfun_unfold [A]. - - Definition zenon_recfun_unfold_s := - fun A P a b eqn c h => @zenon_recfun_unfold A P a b eqn h c - . --Implicit Arguments zenon_recfun_unfold_s [A]. -+Arguments zenon_recfun_unfold_s [A]. diff --git a/zenon-ocaml.patch b/zenon-ocaml.patch deleted file mode 100644 index c03e325..0000000 --- a/zenon-ocaml.patch +++ /dev/null @@ -1,55 +0,0 @@ ---- coqterm.ml.orig 2018-09-18 09:01:37.000000000 -0600 -+++ coqterm.ml 2020-08-20 13:02:03.239490105 -0600 -@@ -447,7 +447,7 @@ let rec rm_lambdas l term = - | _, _ -> assert false - ;; - --let compare_hyps (name1, _) (name2, _) = Pervasives.compare name1 name2;; -+let compare_hyps (name1, _) (name2, _) = Stdlib.compare name1 name2;; - - let make_lemma { name = name; params = params; proof = proof } = - let f (ty, e) = ---- expr.ml.orig 2018-09-18 09:01:37.000000000 -0600 -+++ expr.ml 2020-08-20 13:01:38.415478986 -0600 -@@ -364,7 +364,7 @@ let hash = get_hash;; - let equal = (==);; - let compare x y = - match compare (hash x) (hash y) with -- | 0 -> if equal x y then 0 else Pervasives.compare x y -+ | 0 -> if equal x y then 0 else Stdlib.compare x y - | x when x < 0 -> -1 - | _ -> 1 - ;; ---- ext_induct.ml.orig 2018-09-18 09:01:37.000000000 -0600 -+++ ext_induct.ml 2020-08-20 13:03:10.847520391 -0600 -@@ -96,8 +96,8 @@ let rec make_case accu e = - - let compare_cases (cs1, _, _) (cs2, _, _) = - try -- Pervasives.compare (Hashtbl.find constructor_table cs1).cd_num -- (Hashtbl.find constructor_table cs2).cd_num -+ Stdlib.compare (Hashtbl.find constructor_table cs1).cd_num -+ (Hashtbl.find constructor_table cs2).cd_num - with Not_found -> raise Empty - ;; - ---- lltoisar.ml.orig 2018-09-18 09:01:37.000000000 -0600 -+++ lltoisar.ml 2020-08-20 13:02:41.168507098 -0600 -@@ -21,7 +21,7 @@ let dict_empty = Dict.empty;; - - module Int = struct - type t = int;; -- let compare = Pervasives.compare;; -+ let compare = Stdlib.compare;; - end;; - module Hypdict = Map.Make (Int);; - -@@ -973,7 +973,7 @@ let rec get_nary_rules accu prf = - let add_nary_rules oc lemmas = - let f lem = get_nary_rules [] lem.proof in - let rules = List.flatten (List.map f lemmas) in -- let rules1 = Misc.list_sort_unique Pervasives.compare rules in -+ let rules1 = Misc.list_sort_unique Stdlib.compare rules in - let f r = - match r with - | Nary_case (n, oth) -> Isar_case.print_case "have" n oth oc diff --git a/zenon.spec b/zenon.spec index 99c4814..f3f460b 100644 --- a/zenon.spec +++ b/zenon.spec @@ -1,11 +1,11 @@ %ifnarch %{ocaml_native_compiler} %global debug_package %{nil} %endif -%global coqver 8.13.2 +%global coqver 8.14.0 Name: zenon -Version: 0.8.4 -Release: 27%{?dist} +Version: 0.8.5 +Release: 1%{?dist} Summary: Automated theorem prover for first-order classical logic License: BSD URL: http://zenon-prover.org/ @@ -16,10 +16,6 @@ Source3: %{name}-tptp-ReadMe # Basic documentation (man pages). Submitted upstream 2008-07-25: Source4: %{name}.1 Source5: %{name}-format.5 -# Adapt to coq 8.9 -Patch0: %{name}-coq89.patch -# Adapt to ocaml 4.08 and later -Patch1: %{name}-ocaml.patch BuildRequires: coq = %{coqver} BuildRequires: ghostscript @@ -38,7 +34,7 @@ generate Coq proofs (proof scripts or proof terms), which can be reinserted into Coq specifications. Zenon can also be extended. %prep -%autosetup -p0 +%autosetup cp -p %{SOURCE1} . @@ -96,6 +92,10 @@ fi %{_mandir}/man5/* %changelog +* Thu Oct 21 2021 Jerry James - 0.8.5-1 +- Version 0.8.5 +- Drop upstreamed -coq89 and -ocaml patches + * Tue Oct 05 2021 Richard W.M. Jones - 0.8.4-27 - OCaml 4.13.1 build From b58f937d3c6b06ffa9652f85ef5d5865acdf3455 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Tue, 30 Nov 2021 13:19:10 -0700 Subject: [PATCH 17/66] Rebuild for coq 8.14.1. --- zenon.spec | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/zenon.spec b/zenon.spec index f3f460b..7ce7fda 100644 --- a/zenon.spec +++ b/zenon.spec @@ -1,11 +1,11 @@ %ifnarch %{ocaml_native_compiler} %global debug_package %{nil} %endif -%global coqver 8.14.0 +%global coqver 8.14.1 Name: zenon Version: 0.8.5 -Release: 1%{?dist} +Release: 2%{?dist} Summary: Automated theorem prover for first-order classical logic License: BSD URL: http://zenon-prover.org/ @@ -92,6 +92,9 @@ fi %{_mandir}/man5/* %changelog +* Tue Nov 30 2021 Jerry James - 0.8.5-2 +- Rebuild for coq 8.14.1 + * Thu Oct 21 2021 Jerry James - 0.8.5-1 - Version 0.8.5 - Drop upstreamed -coq89 and -ocaml patches From 999621128e24f4284e9ae710c76d92337c10c0ec Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Sat, 22 Jan 2022 05:49:58 +0000 Subject: [PATCH 18/66] - Rebuilt for https://fedoraproject.org/wiki/Fedora_36_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 7ce7fda..790b9c2 100644 --- a/zenon.spec +++ b/zenon.spec @@ -5,7 +5,7 @@ Name: zenon Version: 0.8.5 -Release: 2%{?dist} +Release: 3%{?dist} Summary: Automated theorem prover for first-order classical logic License: BSD URL: http://zenon-prover.org/ @@ -92,6 +92,9 @@ fi %{_mandir}/man5/* %changelog +* Sat Jan 22 2022 Fedora Release Engineering - 0.8.5-3 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_36_Mass_Rebuild + * Tue Nov 30 2021 Jerry James - 0.8.5-2 - Rebuild for coq 8.14.1 From c55b03b328910832ffdc51e659d89515d07a5905 Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Fri, 4 Feb 2022 17:36:09 +0000 Subject: [PATCH 19/66] OCaml 4.13.1 rebuild to remove package notes --- zenon.spec | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/zenon.spec b/zenon.spec index 790b9c2..048dbf7 100644 --- a/zenon.spec +++ b/zenon.spec @@ -1,3 +1,4 @@ +%undefine _package_note_flags %ifnarch %{ocaml_native_compiler} %global debug_package %{nil} %endif @@ -5,7 +6,7 @@ Name: zenon Version: 0.8.5 -Release: 3%{?dist} +Release: 4%{?dist} Summary: Automated theorem prover for first-order classical logic License: BSD URL: http://zenon-prover.org/ @@ -92,6 +93,9 @@ fi %{_mandir}/man5/* %changelog +* Fri Feb 04 2022 Richard W.M. Jones - 0.8.5-4 +- OCaml 4.13.1 rebuild to remove package notes + * Sat Jan 22 2022 Fedora Release Engineering - 0.8.5-3 - Rebuilt for https://fedoraproject.org/wiki/Fedora_36_Mass_Rebuild From 62ad34fcdc179f0821cdf68093739be5d58be90c Mon Sep 17 00:00:00 2001 From: Jerry James Date: Mon, 28 Feb 2022 19:35:15 -0700 Subject: [PATCH 20/66] Rebuild for coq 8.15.0. --- zenon.rpmlintrc | 8 -------- zenon.spec | 8 ++++++-- 2 files changed, 6 insertions(+), 10 deletions(-) delete mode 100644 zenon.rpmlintrc diff --git a/zenon.rpmlintrc b/zenon.rpmlintrc deleted file mode 100644 index cd62189..0000000 --- a/zenon.rpmlintrc +++ /dev/null @@ -1,8 +0,0 @@ -# THIS FILE IS FOR WHITELISTING RPMLINT ERRORS AND WARNINGS IN TASKOTRON -# https://fedoraproject.org/wiki/Taskotron/Tasks/dist.rpmlint#Whitelisting_errors - -# The dictionary is missing some technical terms -addFilter(r'W: spelling-error .* prover') - -# The configure script is not an autotools-generated script -addFilter(r'zenon\.spec:[^:]*: W: configure-without-libdir-spec') diff --git a/zenon.spec b/zenon.spec index 048dbf7..d4688eb 100644 --- a/zenon.spec +++ b/zenon.spec @@ -1,12 +1,13 @@ %undefine _package_note_flags + %ifnarch %{ocaml_native_compiler} %global debug_package %{nil} %endif -%global coqver 8.14.1 +%global coqver 8.15.0 Name: zenon Version: 0.8.5 -Release: 4%{?dist} +Release: 5%{?dist} Summary: Automated theorem prover for first-order classical logic License: BSD URL: http://zenon-prover.org/ @@ -93,6 +94,9 @@ fi %{_mandir}/man5/* %changelog +* Mon Feb 28 2022 Jerry James - 0.8.5-5 +- Rebuild for coq 8.15.0 + * Fri Feb 04 2022 Richard W.M. Jones - 0.8.5-4 - OCaml 4.13.1 rebuild to remove package notes From 388a4c5f10e3367d5bc04f9955b93fb7dca62cc4 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Fri, 25 Mar 2022 11:40:29 -0600 Subject: [PATCH 21/66] Rebuild for coq 8.15.1. --- zenon.spec | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/zenon.spec b/zenon.spec index d4688eb..a6c07fd 100644 --- a/zenon.spec +++ b/zenon.spec @@ -3,11 +3,11 @@ %ifnarch %{ocaml_native_compiler} %global debug_package %{nil} %endif -%global coqver 8.15.0 +%global coqver 8.15.1 Name: zenon Version: 0.8.5 -Release: 5%{?dist} +Release: 6%{?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 +* Fri Mar 25 2022 Jerry James - 0.8.5-6 +- Rebuild for coq 8.15.1 + * Mon Feb 28 2022 Jerry James - 0.8.5-5 - Rebuild for coq 8.15.0 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 22/66] 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 23/66] 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 24/66] 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 25/66] 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 26/66] 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 27/66] 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 28/66] 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 29/66] 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 30/66] 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 31/66] 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 32/66] 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 33/66] 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 34/66] 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 35/66] 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 36/66] 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 37/66] 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 38/66] 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 39/66] 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 40/66] 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 41/66] 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 42/66] 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 43/66] 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 44/66] 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 45/66] 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 46/66] 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 47/66] 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 48/66] 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 49/66] 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 50/66] 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 51/66] 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 52/66] 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 53/66] 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 54/66] 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 55/66] 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 56/66] 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 57/66] 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 58/66] 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 59/66] 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 60/66] 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 61/66] 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 62/66] 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 63/66] 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 64/66] 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 65/66] 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 66/66] 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