Name: zenon
Version: 0.5.0
Release: 7%{?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
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
%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.
%prep
%setup -q -n zenon
%patch0
%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}
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
# 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
%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}
%endif
%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/
%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`
if [ "$result" = "(* PROOF-FOUND *)" ] ; then
echo "Test succeeded"
else
echo "TEST FAILED"
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}/
%{_mandir}/man1/*
%{_mandir}/man5/*
%changelog
* Tue Sep 22 2009 Dennis gilmore <dennis@ausil.us> - 0.5.0-7
- ExcludeArch sparc64 no ocaml
* Tue Aug 11 2009 Ville Skyttä <ville.skytta@iki.fi> - 0.5.0-6
- Use bzipped upstream tarball.
* Mon Jul 27 2009 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 0.5.0-5.1
- Rebuilt for https://fedoraproject.org/wiki/Fedora_12_Mass_Rebuild
* Mon Jun 15 2009 Karsten Hopp <karsten@redhat.com> 0.5.0-4.1
- ocaml not available on mainframes, add excludearch
* Wed Feb 25 2009 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 0.5.0-4
- Rebuilt for https://fedoraproject.org/wiki/Fedora_11_Mass_Rebuild
* Fri Jun 27 2008 David A. Wheeler - 0.5.0-3
- Add documentation for Zenon and its built-in format as man pages
(man pages used so Debian, etc., will use them too)
- Fix release number so it increases everywhere
* Fri Jun 27 2008 David A. Wheeler - 0.5.0-2.1
- macro fc8 failed, minor rebuild for Fedora 8
* Fri Jun 27 2008 David A. Wheeler - 0.5.0-2
- Moved examples to an "examples" subdirectory in /usr/share/doc/NAME-VERSION
- Moved "check" to be after "install" in spec file (that's when it's executed)
- Exclude ppc64 for Fedora 8 (it works on 9 and 10, but not 8)
* Fri Jun 27 2008 David A. Wheeler - 0.5.0-1
- Initial package
