Rebuild for coq 8.17.1

2023-10-18 09:48:32 -06:00
2 changed files with 30 additions and 139 deletions
--- a/zenon-deprecated.patch
+++ b/zenon-deprecated.patch
@ -1,34 +0,0 @@
--- zenon-0.8.5/zenon_coqbool.v.orig	2020-10-23 09:19:07.000000000 -0600
-+++ zenon-0.8.5/zenon_coqbool.v	2026-03-03 16:33:33.636474063 -0700
-@@ -1,6 +1,6 @@
- (*  Copyright 2004 INRIA  *)
- 
-Require Export Bool.
-+From Stdlib Require Export Bool.
- 
- Definition __g_not_b := negb.
- Definition __g_and_b := andb.
--- zenon-0.8.5/zenon_focal.v.orig	2020-10-23 09:19:07.000000000 -0600
-+++ zenon-0.8.5/zenon_focal.v	2026-03-03 16:34:30.531982864 -0700
-@@ -1,8 +1,8 @@
- (*  Copyright 2004 INRIA  *)
- 
-Require Export Bool.
-Require Import ClassicalEpsilon.
-Require List.
-+From Stdlib Require Export Bool.
-+From Stdlib Require Import ClassicalEpsilon.
-+From Stdlib Require List.
- 
- (* magic: this whole file depends on the following definitions:
-    basics.and_b := andb
--- zenon-0.8.5/zenon.v.orig	2020-10-23 09:19:07.000000000 -0600
-+++ zenon-0.8.5/zenon.v	2026-03-03 16:33:06.988515450 -0700
-@@ -1,6 +1,6 @@
- (*  Copyright 2004 INRIA  *)
- 
-Require Export Classical.
-+From Stdlib Require Export Classical.
- 
- Lemma zenon_notnot : forall P : Prop,
-   P -> (~ P -> False).
--- a/zenon.spec
+++ b/zenon.spec
@ -1,46 +1,46 @@
+%undefine _package_note_flags
+
+%ifnarch %{ocaml_native_compiler}
 %global debug_package %{nil}
-%global rocqver 9.2.0
-%global giturl  https://github.com/zenon-prover/zenon
+%endif
+%global coqver 8.17.1

 Name:		zenon
 Version:	0.8.5
-Release:	43%{?dist}
+Release:	16%{?dist}
 Summary:	Automated theorem prover for first-order classical logic
 License:	BSD-3-Clause
 URL:		http://zenon-prover.org/
-VCS:		git:%{giturl}.git
-Source0:	%{giturl}/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
 # 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}
+# ANTLR is unavailable on i686, so coq is also unavailable
+# See https://fedoraproject.org/wiki/Changes/Drop_i686_JDKs
+ExclusiveArch:  %{java_arches}

-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 +54,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,89 +98,8 @@ fi
 %{_mandir}/man5/zenon-format.5*

 %changelog
-* Wed Jul 29 2026 Jerry James <loganjerry@gmail.com> - 0.8.5-43
- Rebuild to fix rocq dependencies
-
-* Fri Jul 17 2026 Fedora Release Engineering <releng@fedoraproject.org> - 0.8.5-42
- Rebuilt for https://fedoraproject.org/wiki/Fedora_45_Mass_Rebuild
-
-* Thu Jul 09 2026 Jerry James <loganjerry@gmail.com> - 0.8.5-41
- OCaml 5.5.0 rebuild
-
-* Thu Apr 16 2026 Jerry James <loganjerry@gmail.com> - 0.8.5-40
- Rebuild for rocq 9.2.0
-
-* Thu Mar 19 2026 Jerry James <loganjerry@gmail.com> - 0.8.5-39
- Rebuild for rocq 9.1.1
-
-* Fri Feb 20 2026 Richard W.M. Jones <rjones@redhat.com> - 0.8.5-38
- OCaml 5.4.1 rebuild
-
-* Sat Jan 17 2026 Fedora Release Engineering <releng@fedoraproject.org> - 0.8.5-37
- Rebuilt for https://fedoraproject.org/wiki/Fedora_44_Mass_Rebuild
-
-* Tue Oct 14 2025 Richard W.M. Jones <rjones@redhat.com> - 0.8.5-36
- OCaml 5.4.0 rebuild
-
-* Fri Aug 22 2025 Jerry James <loganjerry@gmail.com> - 0.8.5-35
- Bump and rebuild
-
-* Sun Aug 10 2025 Jerry James <loganjerry@gmail.com> - 0.8.5-34
- Bump and rebuild
-
-* Fri Jul 25 2025 Fedora Release Engineering <releng@fedoraproject.org> - 0.8.5-33
- Rebuilt for https://fedoraproject.org/wiki/Fedora_43_Mass_Rebuild
-
-* Sat Jul 12 2025 Jerry James <loganjerry@gmail.com> - 0.8.5-32
- Rebuild to fix OCaml dependencies
-
-* Wed Jan 22 2025 Jerry James <loganjerry@gmail.com> - 0.8.5-31
- Rebuild for coq 8.20.1
-
-* Sun Jan 19 2025 Fedora Release Engineering <releng@fedoraproject.org> - 0.8.5-30
- Rebuilt for https://fedoraproject.org/wiki/Fedora_42_Mass_Rebuild
-
-* Fri Jan 10 2025 Jerry James <loganjerry@gmail.com> - 0.8.5-29
- OCaml 5.3.0 rebuild for Fedora 42
-
-* Sat Jul 20 2024 Fedora Release Engineering <releng@fedoraproject.org> - 0.8.5-28
- Rebuilt for https://fedoraproject.org/wiki/Fedora_41_Mass_Rebuild
-
-* Wed Jun 19 2024 Richard W.M. Jones <rjones@redhat.com> - 0.8.5-27
- OCaml 5.2.0 ppc64le fix
-
-* Wed May 29 2024 Richard W.M. Jones <rjones@redhat.com> - 0.8.5-26
- OCaml 5.2.0 for Fedora 41
-
-* Fri Feb  2 2024 Jerry James <loganjerry@gmail.com> - 0.8.5-25
- Rebuild for rebuilt coq
-
-* Sat Jan 27 2024 Fedora Release Engineering <releng@fedoraproject.org> - 0.8.5-24
- Rebuilt for https://fedoraproject.org/wiki/Fedora_40_Mass_Rebuild
-
-* Tue Jan  2 2024 Jerry James <loganjerry@gmail.com> - 0.8.5-23
- Rebuild for coq 8.18.0
-
-* Mon Dec 18 2023 Richard W.M. Jones <rjones@redhat.com> - 0.8.5-22
- OCaml 5.1.1 + s390x code gen fix for Fedora 40
-
-* Tue Dec 12 2023 Richard W.M. Jones <rjones@redhat.com> - 0.8.5-21
- OCaml 5.1.1 rebuild for Fedora 40
-
-* Thu Oct 05 2023 Richard W.M. Jones <rjones@redhat.com> - 0.8.5-20
- OCaml 5.1 rebuild for Fedora 40
-
-* Thu Jul 27 2023 Jerry James <loganjerry@gmail.com> - 0.8.5-19
- Rebuild for ocaml-zarith 1.13
-
-* Sat Jul 22 2023 Fedora Release Engineering <releng@fedoraproject.org> - 0.8.5-18
- Rebuilt for https://fedoraproject.org/wiki/Fedora_39_Mass_Rebuild
-
-* Wed Jul 12 2023 Richard W.M. Jones <rjones@redhat.com> - 0.8.5-17
- OCaml 5.0 rebuild for Fedora 39
-
-* Mon Jul 10 2023 Jerry James <loganjerry@gmail.com> - 0.8.5-16
- OCaml 5.0.0 rebuild
+* Wed Oct 18 2023 Jerry James <loganjerry@gmail.com> - 0.8.5-16
+- Rebuild for coq 8.17.1

 * Sat Apr  1 2023 Jerry James <loganjerry@gmail.com> - 0.8.5-15
 - Rebuild for coq 8.17.0