Compare commits
No commits in common. "rawhide" and "f28" have entirely different histories.
5 changed files with 35 additions and 301 deletions
4
.gitignore
vendored
4
.gitignore
vendored
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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.
|
||||
4
sources
4
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
|
||||
|
|
|
|||
|
|
@ -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).
|
||||
285
zenon.spec
285
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 <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
|
||||
|
||||
* Sat Apr 1 2023 Jerry James <loganjerry@gmail.com> - 0.8.5-15
|
||||
- Rebuild for coq 8.17.0
|
||||
|
||||
* Tue Jan 24 2023 Richard W.M. Jones <rjones@redhat.com> - 0.8.5-14
|
||||
- Bump release and rebuild
|
||||
|
||||
* Tue Jan 24 2023 Richard W.M. Jones <rjones@redhat.com> - 0.8.5-13
|
||||
- Rebuild OCaml packages for F38
|
||||
|
||||
* Sat Jan 21 2023 Fedora Release Engineering <releng@fedoraproject.org> - 0.8.5-12
|
||||
- Rebuilt for https://fedoraproject.org/wiki/Fedora_38_Mass_Rebuild
|
||||
|
||||
* Sat Nov 26 2022 Jerry James <loganjerry@gmail.com> - 0.8.5-11
|
||||
- Rebuild for coq 8.16.1
|
||||
|
||||
* Fri Sep 16 2022 Jerry James <loganjerry@gmail.com> - 0.8.5-10
|
||||
- Rebuild for coq 8.16.0
|
||||
|
||||
* Thu Aug 18 2022 Jerry James <loganjerry@gmail.com> - 0.8.5-9
|
||||
- Rebuild to fix coq dependency
|
||||
- Convert License tag to SPDX
|
||||
|
||||
* Sat Jul 23 2022 Fedora Release Engineering <releng@fedoraproject.org> - 0.8.5-8
|
||||
- Rebuilt for https://fedoraproject.org/wiki/Fedora_37_Mass_Rebuild
|
||||
|
||||
* Wed Jul 20 2022 Jerry James <loganjerry@gmail.com> - 0.8.5-7
|
||||
- Remove i686 support
|
||||
|
||||
* Sun Jun 19 2022 Richard W.M. Jones <rjones@redhat.com> - 0.8.5-7
|
||||
- OCaml 4.14.0 rebuild
|
||||
|
||||
* Fri Mar 25 2022 Jerry James <loganjerry@gmail.com> - 0.8.5-6
|
||||
- Rebuild for coq 8.15.1
|
||||
|
||||
* Mon Feb 28 2022 Jerry James <loganjerry@gmail.com> - 0.8.5-5
|
||||
- Rebuild for coq 8.15.0
|
||||
|
||||
* Fri Feb 04 2022 Richard W.M. Jones <rjones@redhat.com> - 0.8.5-4
|
||||
- OCaml 4.13.1 rebuild to remove package notes
|
||||
|
||||
* Sat Jan 22 2022 Fedora Release Engineering <releng@fedoraproject.org> - 0.8.5-3
|
||||
- Rebuilt for https://fedoraproject.org/wiki/Fedora_36_Mass_Rebuild
|
||||
|
||||
* Tue Nov 30 2021 Jerry James <loganjerry@gmail.com> - 0.8.5-2
|
||||
- Rebuild for coq 8.14.1
|
||||
|
||||
* Thu Oct 21 2021 Jerry James <loganjerry@gmail.com> - 0.8.5-1
|
||||
- Version 0.8.5
|
||||
- Drop upstreamed -coq89 and -ocaml patches
|
||||
|
||||
* Tue Oct 05 2021 Richard W.M. Jones <rjones@redhat.com> - 0.8.4-27
|
||||
- OCaml 4.13.1 build
|
||||
|
||||
* Mon Oct 04 2021 Richard W.M. Jones <rjones@redhat.com> - 0.8.4-26
|
||||
- Try to build on s390x with OCaml 4.13
|
||||
|
||||
* Fri Jul 23 2021 Fedora Release Engineering <releng@fedoraproject.org> - 0.8.4-25
|
||||
- Rebuilt for https://fedoraproject.org/wiki/Fedora_35_Mass_Rebuild
|
||||
|
||||
* Tue Jun 8 2021 Jerry James <loganjerry@gmail.com> - 0.8.4-24
|
||||
- Rebuild for coq 8.13.2
|
||||
|
||||
* Wed Mar 3 2021 Jerry James <loganjerry@gmail.com> - 0.8.4-23
|
||||
- Rebuild for coq 8.13.1
|
||||
|
||||
* Tue Mar 2 11:03:37 GMT 2021 Richard W.M. Jones <rjones@redhat.com> - 0.8.4-22
|
||||
- OCaml 4.12.0 build
|
||||
|
||||
* Sat Feb 20 2021 Jerry James <loganjerry@gmail.com> - 0.8.4-21
|
||||
- Rebuild for coq 8.13.0
|
||||
|
||||
* Thu Jan 28 2021 Fedora Release Engineering <releng@fedoraproject.org> - 0.8.4-20
|
||||
- Rebuilt for https://fedoraproject.org/wiki/Fedora_34_Mass_Rebuild
|
||||
|
||||
* Wed Dec 23 2020 Jerry James <loganjerry@gmail.com> - 0.8.4-19
|
||||
- Rebuild for coq 8.12.2
|
||||
|
||||
* Wed Dec 2 2020 Jerry James <loganjerry@gmail.com> - 0.8.4-18
|
||||
- Rebuild for coq 8.12.1
|
||||
|
||||
* Wed Sep 02 2020 Richard W.M. Jones <rjones@redhat.com> - 0.8.4-17
|
||||
- OCaml 4.11.1 rebuild
|
||||
|
||||
* Tue Sep 1 2020 Jerry James <loganjerry@gmail.com> - 0.8.4-16
|
||||
- Rebuild for coq 8.12.0
|
||||
|
||||
* Sat Aug 22 2020 Richard W.M. Jones <rjones@redhat.com> - 0.8.4-16
|
||||
- OCaml 4.11.0 rebuild
|
||||
|
||||
* Sat Aug 01 2020 Fedora Release Engineering <releng@fedoraproject.org> - 0.8.4-15
|
||||
- Second attempt - Rebuilt for
|
||||
https://fedoraproject.org/wiki/Fedora_33_Mass_Rebuild
|
||||
|
||||
* Wed Jul 29 2020 Fedora Release Engineering <releng@fedoraproject.org> - 0.8.4-14
|
||||
- Rebuilt for https://fedoraproject.org/wiki/Fedora_33_Mass_Rebuild
|
||||
|
||||
* Mon Jun 15 2020 Jerry James <loganjerry@gmail.com> - 0.8.4-13
|
||||
- Rebuild for coq 8.11.2
|
||||
|
||||
* Wed May 20 2020 Jerry James <loganjerry@gmail.com> - 0.8.4-12
|
||||
- Rebuild for coq 8.11.1
|
||||
|
||||
* Tue May 05 2020 Richard W.M. Jones <rjones@redhat.com> - 0.8.4-11
|
||||
- OCaml 4.11.0+dev2-2020-04-22 rebuild
|
||||
|
||||
* Sat Apr 04 2020 Richard W.M. Jones <rjones@redhat.com> - 0.8.4-10
|
||||
- Update all OCaml dependencies for RPM 4.16.
|
||||
|
||||
* Mon Mar 23 2020 Jerry James <loganjerry@gmail.com> - 0.8.4-9
|
||||
- Rebuild for coq 8.11.0
|
||||
|
||||
* Fri Jan 31 2020 Fedora Release Engineering <releng@fedoraproject.org> - 0.8.4-8
|
||||
- Rebuilt for https://fedoraproject.org/wiki/Fedora_32_Mass_Rebuild
|
||||
|
||||
* Wed Jan 22 2020 Jerry James <loganjerry@gmail.com> - 0.8.4-7
|
||||
- OCaml 4.10.0+beta1 rebuild.
|
||||
|
||||
* Fri Sep 6 2019 Jerry James <loganjerry@gmail.com> - 0.8.4-6
|
||||
- OCaml 4.08.1 (final) rebuild.
|
||||
|
||||
* Thu Aug 1 2019 Jerry James <loganjerry@gmail.com> - 0.8.4-5
|
||||
- OCaml 4.08.1 (rc2) rebuild.
|
||||
|
||||
* Sat Jul 27 2019 Fedora Release Engineering <releng@fedoraproject.org> - 0.8.4-4
|
||||
- Rebuilt for https://fedoraproject.org/wiki/Fedora_31_Mass_Rebuild
|
||||
|
||||
* Wed Jun 5 2019 Jerry James <loganjerry@gmail.com> - 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 <releng@fedoraproject.org> - 0.8.4-2
|
||||
- Rebuilt for https://fedoraproject.org/wiki/Fedora_30_Mass_Rebuild
|
||||
|
||||
* Sat Jan 26 2019 Jerry James <loganjerry@gmail.com> - 0.8.4-1
|
||||
- New upstream release
|
||||
- Drop -unsafe-string workaround
|
||||
|
||||
* Sat Jul 14 2018 Fedora Release Engineering <releng@fedoraproject.org> - 0.8.2-12
|
||||
- Rebuilt for https://fedoraproject.org/wiki/Fedora_29_Mass_Rebuild
|
||||
|
||||
* Mon Feb 12 2018 Jerry James <loganjerry@gmail.com> - 0.8.2-11
|
||||
- Rebuild for coq 8.7.1
|
||||
- Compile with -unsafe-string until the code can be migrated
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue