diff --git a/zenon-deprecated.patch b/zenon-deprecated.patch deleted file mode 100644 index a4bf9fa..0000000 --- a/zenon-deprecated.patch +++ /dev/null @@ -1,34 +0,0 @@ ---- zenon-0.8.5/zenon_coqbool.v.orig 2020-10-23 09:19:07.000000000 -0600 -+++ zenon-0.8.5/zenon_coqbool.v 2026-03-03 16:33:33.636474063 -0700 -@@ -1,6 +1,6 @@ - (* Copyright 2004 INRIA *) - --Require Export Bool. -+From Stdlib Require Export Bool. - - Definition __g_not_b := negb. - Definition __g_and_b := andb. ---- zenon-0.8.5/zenon_focal.v.orig 2020-10-23 09:19:07.000000000 -0600 -+++ zenon-0.8.5/zenon_focal.v 2026-03-03 16:34:30.531982864 -0700 -@@ -1,8 +1,8 @@ - (* Copyright 2004 INRIA *) - --Require Export Bool. --Require Import ClassicalEpsilon. --Require List. -+From Stdlib Require Export Bool. -+From Stdlib Require Import ClassicalEpsilon. -+From Stdlib Require List. - - (* magic: this whole file depends on the following definitions: - basics.and_b := andb ---- zenon-0.8.5/zenon.v.orig 2020-10-23 09:19:07.000000000 -0600 -+++ zenon-0.8.5/zenon.v 2026-03-03 16:33:06.988515450 -0700 -@@ -1,6 +1,6 @@ - (* Copyright 2004 INRIA *) - --Require Export Classical. -+From Stdlib Require Export Classical. - - Lemma zenon_notnot : forall P : Prop, - P -> (~ P -> False). diff --git a/zenon.spec b/zenon.spec index b208d71..91d2d0d 100644 --- a/zenon.spec +++ b/zenon.spec @@ -1,10 +1,15 @@ +# Coq's plugin architecture requires cmxs files, so: +ExclusiveArch: %{ocaml_native_compiler} + +%ifnarch %{ocaml_native_compiler} %global debug_package %{nil} -%global rocqver 9.2.0 +%endif +%global coqver 8.20.1 %global giturl https://github.com/zenon-prover/zenon Name: zenon Version: 0.8.5 -Release: 43%{?dist} +Release: 31%{?dist} Summary: Automated theorem prover for first-order classical logic License: BSD-3-Clause URL: http://zenon-prover.org/ @@ -16,31 +21,25 @@ Source3: %{name}-tptp-ReadMe # Basic documentation (man pages). Submitted upstream 2008-07-25: Source4: %{name}.1 Source5: %{name}-format.5 -# Update deprecated usage -Patch: %{name}-deprecated.patch -# Rocq's plugin architecture requires cmxs files -ExclusiveArch: %{ocaml_native_compiler} - -BuildRequires: coq-core-compat = %{rocqver} -BuildRequires: rocq = %{rocqver} -BuildRequires: rocq-stdlib +BuildRequires: coq = %{coqver} +BuildRequires: ghostscript +BuildRequires: ImageMagick BuildRequires: make BuildRequires: ocaml -Requires: rocq%{?_isa} = %{rocqver} -Requires: rocq-stdlib%{?_isa} +Requires: coq%{?_isa} = %{coqver} Requires: coreutils %description -Zenon is an automated theorem prover for first order classical logic with -equality, based on the tableau method. Zenon can read input files in TPTP, -Coq, Focal, and its own Zenon format. Zenon can directly generate Coq proofs -(proof scripts or proof terms), which can be reinserted into Coq -specifications. Zenon can also be extended. +Zenon is an automated theorem prover for first order classical logic +with equality, based on the tableau method. Zenon can read input files +in TPTP, Coq, Focal, and its own Zenon format. Zenon can directly +generate Coq proofs (proof scripts or proof terms), which can be +reinserted into Coq specifications. Zenon can also be extended. %prep -%autosetup -p1 +%autosetup cp -p %{SOURCE1} . @@ -54,8 +53,14 @@ mkdir examples cp -p %{SOURCE2} examples/tptp-COM003+2.p cp -p %{SOURCE3} examples/tptp-ReadMe -make %{?_smp_mflags} zenon.bin -cp -p zenon.bin zenon +# Work around Makefile errors (fails if no ocamlopt, uses _bytecode_ otherwise) +%ifarch %{ocaml_native_compiler} + make %{?_smp_mflags} zenon.bin + cp -p zenon.bin zenon +%else + make %{?_smp_mflags} zenon.byt + cp -p zenon.byt zenon +%endif # Use of %%{?_smp_mflags} sometimes leads to build failures make coq @@ -92,42 +97,6 @@ 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