[zenon] New upstream release. Drop unnecessary spec file elements (BuildRoot, etc.). Execstack flag clearing
Jerry James
jjames at fedoraproject.org
Tue Jul 12 22:02:15 UTC 2011
commit 32904f138dc22f8b962e6b349ca73e66df182a8f
Author: Jerry James <loganjerry at gmail.com>
Date: Tue Jul 12 16:01:26 2011 -0600
New upstream release.
Drop unnecessary spec file elements (BuildRoot, etc.).
Execstack flag clearing no longer necessary.
Build on exactly the arches that coq builds on.
Build the icons.
.gitignore | 2 +-
sources | 2 +-
zenon.1 | 2 +-
zenon.bytecode.patch | 11 -----
zenon.spec | 119 +++++++++++++++++++-------------------------------
5 files changed, 48 insertions(+), 88 deletions(-)
---
diff --git a/.gitignore b/.gitignore
index e287582..637832f 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1 +1 @@
-zenon-0.5.0.tar.bz2
+/zenon-0.6.3.tar.bz2
diff --git a/sources b/sources
index 1f5c726..018eb22 100644
--- a/sources
+++ b/sources
@@ -1 +1 @@
-3b5496aac11aa401ffccb422c866a4b6 zenon-0.5.0.tar.bz2
+d1d2a42e8d1b1e5eeed2f6ab8b034c49 zenon-0.6.3.tar.bz2
diff --git a/zenon.1 b/zenon.1
index de96930..ded9b46 100644
--- a/zenon.1
+++ b/zenon.1
@@ -144,7 +144,7 @@ Zenon can prove this, and will print out:
.br
\fC(* BEGIN-PROOF *)\fP
.br
-... details of proof in Coq format
+\&... details of proof in Coq format
.br
\fC(* END-PROOF *)\fP
.RE
diff --git a/zenon.spec b/zenon.spec
index bb72973..25052c6 100644
--- a/zenon.spec
+++ b/zenon.spec
@@ -1,96 +1,71 @@
+# Don't create debuginfo; it's not particularly useful for OCaml programs.
+%global debug_package %{nil}
+%global opt %(test -x %{_bindir}/ocamlopt && echo 1 || echo 0)
+
Name: zenon
-Version: 0.5.0
-Release: 8%{?dist}
+Version: 0.6.3
+Release: 1%{?dist}
Summary: Automated theorem prover for first-order classical logic
Group: Applications/Engineering
License: BSD
-URL: http://focal.inria.fr/zenon
-Source0: http://focal.inria.fr/zenon/zenon-0.5.0.tar.bz2
+URL: http://focal.inria.fr/zenon/
+Source0: http://focal.inria.fr/zenon/zenon-%{version}.tar.bz2
Source1: zenon-tptp-COM003+2.p
Source2: zenon-tptp-ReadMe
# Basic documentation (man pages). Submitted upstream 2008-07-25:
Source3: zenon.1
Source4: zenon-format.5
-Patch0 : zenon.bytecode.patch
-BuildRoot: %{_tmppath}/%{name}-%{version}-%{release}-root-%(%{__id_u} -n)
-BuildRequires: ocaml >= 3.08
-# prelink required to run execstack:
-BuildRequires: prelink
-%if 0%fedora == 8
-ExcludeArch: ppc64
-%endif
-ExcludeArch: s390 s390x sparc64
+
+BuildRequires: coq
+BuildRequires: ghostscript
+BuildRequires: ImageMagick
+BuildRequires: ocaml
+
+# This should always match the list in the coq spec file.
+ExclusiveArch: alpha armv4l %{ix86} ia64 x86_64 ppc sparc sparcv9
%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.
+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
-%setup -q -n zenon
-%patch0
+%setup -q
%build
-%define opt %(test -x %{_bindir}/ocamlopt && echo 1 || echo 0)
-
-# Upstream places libraries in /usr.../lib/NAME, but FHS says to place
-# arch-independent files in /usr/share/NAME. We'll follow FHS.
-# rpmlint bug: rpmlint complains that --libdir isn't specified here, but it is
-bash configure --enable-debug --exec_prefix %{_exec_prefix} \
- --bindir %{_bindir} --libdir %{_datadir}/%{name}
+# The -libdir argument identifies where to put the coq files.
+./configure -prefix %{_prefix} -libdir %{_libdir}/coq/user-contrib -sum md5sum
-cp -p %{SOURCE1} tptp-COM003+2.p
-cp -p %{SOURCE2} tptp-ReadMe
-chmod g-w tptp*
-
-cp -p %{SOURCE3} %{SOURCE4} .
-gzip zenon.1
-gzip zenon-format.5
+mkdir examples
+cp -p %{SOURCE1} examples/tptp-COM003+2.p
+cp -p %{SOURCE2} examples/tptp-ReadMe
# Work around Makefile errors (fails if no ocamlopt, uses _bytecode_ otherwise)
%if %opt
- make %{?_smp_mflags} zenon.opt
- cp zenon.opt zenon
- # Clear executable stack; it's unnecessary and a security problem.
- # See http://caml.inria.fr/mantis/bug_view_page.php?bug_id=4564
- execstack -c zenon
+ make %{?_smp_mflags} zenon.bin coq
+ cp -p zenon.bin zenon
+ strip zenon
%else
- make %{?_smp_mflags} zenon.byt
- cp zenon.byt zenon
- # Suppress creating debug package if we only have bytecode.
- %define _enable_debug_package 0
- %define debug_package %{nil}
- %define __os_install_post /usr/lib/rpm/brp-compress %{nil}
+ make %{?_smp_mflags} zenon.byt coq
+ cp -p zenon.byt zenon
%endif
-
+make -C doc zenon-logo-small.png
%install
-rm -rf %{buildroot}
-install -d %{buildroot}/%{_bindir}/
-install -d %{buildroot}/%{_libdir}/
-
make install DESTDIR=%{buildroot}
-install -d %{buildroot}/%{_defaultdocdir}/%{name}-%{version}/examples/
-cp -p LICENSE %{buildroot}/%{_defaultdocdir}/%{name}-%{version}/
-cp -p tptp-COM003+2.p tptp-ReadMe \
- %{buildroot}/%{_defaultdocdir}/%{name}-%{version}/examples/
-
install -d %{buildroot}%{_mandir}/man1/
install -d %{buildroot}%{_mandir}/man5/
-cp -p zenon.1.gz %{buildroot}%{_mandir}/man1/
-cp -p zenon-format.5.gz %{buildroot}%{_mandir}/man5/
-
-
+cp -p %{SOURCE3} %{buildroot}%{_mandir}/man1/
+cp -p %{SOURCE4} %{buildroot}%{_mandir}/man5/
%check
# Sanity test. Can we prove TPTP v3.4.2 test COM003+2 (the halting problem)?
# tptp-ReadMe has test's license conditions ("must credit + note changes").
# TPTP from: http://www.cs.miami.edu/~tptp/TPTP/Distribution/TPTP-v3.4.2.tgz
-result=`./zenon -p0 -itptp tptp-COM003+2.p`
+result=`./zenon -p0 -itptp examples/tptp-COM003+2.p`
if [ "$result" = "(* PROOF-FOUND *)" ] ; then
echo "Test succeeded"
else
@@ -98,23 +73,21 @@ else
false
fi
-
-
-%clean
-rm -rf %{buildroot}
-
-
-# We can't use %%doc if it has a subdirectory ("examples" in this case)
%files
-%defattr(-,root,root,-)
-%{_defaultdocdir}/%{name}-%{version}/
-%{_bindir}/*
-%{_datadir}/%{name}/
+%doc LICENSE examples doc/*.png
+%{_bindir}/zenon
+%{_libdir}/coq/user-contrib/zenon
%{_mandir}/man1/*
%{_mandir}/man5/*
-
%changelog
+* Tue Jul 12 2011 Jerry James <loganjerry at gmail.com> - 0.6.3-1
+- New upstream release
+- Drop unnecessary spec file elements (BuildRoot, etc.)
+- Execstack flag clearing no longer necessary
+- Build on exactly the arches that coq builds on
+- Build the icons
+
* Tue Feb 08 2011 Fedora Release Engineering <rel-eng at lists.fedoraproject.org> - 0.5.0-8
- Rebuilt for https://fedoraproject.org/wiki/Fedora_15_Mass_Rebuild
@@ -148,5 +121,3 @@ rm -rf %{buildroot}
* Fri Jun 27 2008 David A. Wheeler - 0.5.0-1
- Initial package
-
-
More information about the scm-commits
mailing list