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 0fb97e5..b208d71 100644 --- a/zenon.spec +++ b/zenon.spec @@ -1,43 +1,46 @@ -# Coq's plugin architecture requires cmxs files, so: -ExclusiveArch: %{ocaml_native_compiler} - -%ifnarch %{ocaml_native_compiler} %global debug_package %{nil} -%endif -%global coqver 8.18.0 +%global rocqver 9.2.0 +%global giturl https://github.com/zenon-prover/zenon Name: zenon Version: 0.8.5 -Release: 25%{?dist} +Release: 43%{?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: 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 # 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} -BuildRequires: ghostscript -BuildRequires: ImageMagick +# Rocq's plugin architecture requires cmxs files +ExclusiveArch: %{ocaml_native_compiler} + +BuildRequires: coq-core-compat = %{rocqver} +BuildRequires: rocq = %{rocqver} +BuildRequires: rocq-stdlib BuildRequires: make BuildRequires: ocaml -Requires: coq%{?_isa} = %{coqver} +Requires: rocq%{?_isa} = %{rocqver} +Requires: rocq-stdlib%{?_isa} 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 +%autosetup -p1 cp -p %{SOURCE1} . @@ -51,14 +54,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 @@ -95,6 +92,60 @@ 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 + +* 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 + +* 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 + +* 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 + +* 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 + +* 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 + +* 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 + +* 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 + +* 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 + * Fri Feb 2 2024 Jerry James - 0.8.5-25 - Rebuild for rebuilt coq