diff --git a/.gitignore b/.gitignore index 9b40f4e..e33b14c 100644 --- a/.gitignore +++ b/.gitignore @@ -1,2 +1,4 @@ /zenlpar07.pdf -/zenon-*.tar.gz +/zenon-0.8.0.tar.gz +/zenon-0.8.1.tar.gz +/zenon-0.8.2.tar.gz diff --git a/README.md b/README.md deleted file mode 100644 index 92f51c8..0000000 --- a/README.md +++ /dev/null @@ -1,9 +0,0 @@ -# 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 bf4128f..183657e 100644 --- a/sources +++ b/sources @@ -1,2 +1,2 @@ -SHA512 (zenon-0.8.5.tar.gz) = dc97cc02bcc2e76a1130f4f7e44ba9839126b5e15f4488ac32d47aef330cbb9ea8c2f1b34f8543ed243587e95848a7187c003a300feed0da64ec81f4501b3bdb -SHA512 (zenlpar07.pdf) = f8a24ba1c32015ea315946042b39f0b629094553097f43c8fb37041450d39b64e3a781006bdcbae42919104907efec9f0cf065d675f3ff09af891d9d28c2549f +f4b8f0fb556c9593069951d6632b519c zenon-0.8.2.tar.gz +068d0f86748914e2c0651f7978a17779 zenlpar07.pdf 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..373f5c2 100644 --- a/zenon.spec +++ b/zenon.spec @@ -1,51 +1,44 @@ +%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.7.1 Name: zenon -Version: 0.8.5 -Release: 43%{?dist} +Version: 0.8.2 +Release: 11%{?dist} Summary: Automated theorem prover for first-order classical logic -License: BSD-3-Clause +License: BSD URL: http://zenon-prover.org/ -VCS: git:%{giturl}.git -Source0: %{giturl}/archive/%{version}/%{name}-%{version}.tar.gz +Source0: http://zenon-prover.org/%{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} - -BuildRequires: coq-core-compat = %{rocqver} -BuildRequires: rocq = %{rocqver} -BuildRequires: rocq-stdlib -BuildRequires: make +BuildRequires: coq = %{coqver} +BuildRequires: ghostscript +BuildRequires: ImageMagick 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 +%setup -q -n %{name} cp -p %{SOURCE1} . -# Generate debuginfo -sed -i 's/^\(CAMLFLAGS = \).*/\1-g/' Makefile +# Generate debuginfo and don't error out on a warning +sed -i 's/^\(CAMLFLAGS = \).*/\1-g -unsafe-string/' Makefile %build ./configure -prefix %{_prefix} -libdir %{_datadir}/%{name} -sum md5sum @@ -54,13 +47,19 @@ 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 %install -%make_install +make install DESTDIR=%{buildroot} install -d %{buildroot}%{_mandir}/man1/ install -d %{buildroot}%{_mandir}/man5/ @@ -88,234 +87,10 @@ fi %license LICENSE %{_bindir}/%{name} %{_libdir}/coq/user-contrib/Zenon -%{_mandir}/man1/zenon.1* -%{_mandir}/man5/zenon-format.5* +%{_mandir}/man1/* +%{_mandir}/man5/* %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 - -* 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 - -* 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 - -* 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 - -* 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 - -* 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 - -* 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 - -* 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 - -* 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 - -* 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 - -* 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 - -* 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 - -* 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 - -* 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 - -* 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 - -* 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 - -* 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 - -* 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 - -* 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 - -* Tue Sep 1 2020 Jerry James - 0.8.4-16 -- Rebuild for coq 8.12.0 - -* Sat Aug 22 2020 Richard W.M. Jones - 0.8.4-16 -- OCaml 4.11.0 rebuild - -* Sat Aug 01 2020 Fedora Release Engineering - 0.8.4-15 -- Second attempt - Rebuilt for - https://fedoraproject.org/wiki/Fedora_33_Mass_Rebuild - -* Wed Jul 29 2020 Fedora Release Engineering - 0.8.4-14 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_33_Mass_Rebuild - -* Mon Jun 15 2020 Jerry James - 0.8.4-13 -- Rebuild for coq 8.11.2 - -* Wed May 20 2020 Jerry James - 0.8.4-12 -- Rebuild for coq 8.11.1 - -* Tue May 05 2020 Richard W.M. Jones - 0.8.4-11 -- OCaml 4.11.0+dev2-2020-04-22 rebuild - -* Sat Apr 04 2020 Richard W.M. Jones - 0.8.4-10 -- Update all OCaml dependencies for RPM 4.16. - -* Mon Mar 23 2020 Jerry James - 0.8.4-9 -- Rebuild for coq 8.11.0 - -* Fri Jan 31 2020 Fedora Release Engineering - 0.8.4-8 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_32_Mass_Rebuild - -* Wed Jan 22 2020 Jerry James - 0.8.4-7 -- OCaml 4.10.0+beta1 rebuild. - -* Fri Sep 6 2019 Jerry James - 0.8.4-6 -- OCaml 4.08.1 (final) rebuild. - -* Thu Aug 1 2019 Jerry James - 0.8.4-5 -- OCaml 4.08.1 (rc2) rebuild. - -* Sat Jul 27 2019 Fedora Release Engineering - 0.8.4-4 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_31_Mass_Rebuild - -* Wed Jun 5 2019 Jerry James - 0.8.4-3 -- Rebuild for coq 8.9.1 -- Add -coq89 patch to adapt to coq 8.9.x - -* Sun Feb 03 2019 Fedora Release Engineering - 0.8.4-2 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_30_Mass_Rebuild - -* Sat Jan 26 2019 Jerry James - 0.8.4-1 -- New upstream release -- Drop -unsafe-string workaround - -* Sat Jul 14 2018 Fedora Release Engineering - 0.8.2-12 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_29_Mass_Rebuild - * Mon Feb 12 2018 Jerry James - 0.8.2-11 - Rebuild for coq 8.7.1 - Compile with -unsafe-string until the code can be migrated