# 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.7.1
Release: 4%{?dist}
Summary: Automated theorem prover for first-order classical logic
Group: Applications/Engineering
License: BSD
URL: http://focal.inria.fr/%{name}/
Source0: http://focal.inria.fr/%{name}/%{name}-%{version}.tar.xz
Source1: http://focal.inria.fr/%{name}/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
BuildRequires: coq
BuildRequires: ghostscript
BuildRequires: ImageMagick
BuildRequires: ocaml
Requires: coq
Requires: coreutils
ExclusiveArch: %{ocaml_arches}
%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
cp -p %{SOURCE1} .
# Fool a script that tries to detect writable directories at config time
sed -i 's/test -w/test -r/' configure
%build
LIB_DIR=%{_datadir}/%{name} \
DOC_DIR=%{_defaultdocdir} \
MAN_DIR=%{_mandir}/man1 \
TOOLS_PROJECT_LIB_DIR=%{_libdir} \
TOOLS_PROJECT_MAN_DIR=%{_mandir} \
TOOLS_PROJECT_DOC_DIR=%{_defaultdocdir} \
CAML_LIB_DIR=%{_libdir}/ocaml \
COQ_LIB_DIR=%{_libdir}/coq \
ZENON_LIB_DIR=%{_datadir}/%{name} \
ZVTOV_LIB_DIR=%{_datadir}/zvtov \
./configure -prefix %{_prefix} -tools_prefix %{_prefix} -coq_rc '~/.coqrc' \
-sum md5sum
mkdir examples
cp -p %{SOURCE2} examples/tptp-COM003+2.p
cp -p %{SOURCE3} examples/tptp-ReadMe
# Work around Makefile errors (fails if no ocamlopt, uses _bytecode_ otherwise)
%if %opt
make %{?_smp_mflags} zenon.bin coq
cp -p zenon.bin zenon
strip zenon
%else
make %{?_smp_mflags} zenon.byt coq
cp -p zenon.byt zenon
%endif
make -C doc zenon-logo-small.png
%install
make install DESTDIR=%{buildroot}
install -d %{buildroot}%{_mandir}/man1/
install -d %{buildroot}%{_mandir}/man5/
cp -p %{SOURCE4} %{buildroot}%{_mandir}/man1/
cp -p %{SOURCE5} %{buildroot}%{_mandir}/man5/
# Remove a symlink and just install the real binary
rm -f %{buildroot}%{_bindir}/%{name}
mv %{buildroot}%{_bindir}/%{name}-%{version} %{buildroot}%{_bindir}/%{name}
# Put the coq files where coq can find them
mkdir -p %{buildroot}%{_libdir}/coq/user-contrib
mv %{buildroot}%{_datadir}/%{name}/%{name}-%{version} \
%{buildroot}%{_libdir}/coq/user-contrib/Zenon
rm -fr %{buildroot}%{_datadir}/%{name}
%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 examples/tptp-COM003+2.p`
if [ "$result" = "(* PROOF-FOUND *)" ] ; then
echo "Test succeeded"
else
echo "TEST FAILED"
false
fi
%files
%doc LICENSE zenlpar07.pdf examples doc/*.png
%{_bindir}/%{name}
%{_libdir}/coq/user-contrib/Zenon
%{_mandir}/man1/*
%{_mandir}/man5/*
%changelog
* Mon Jan 7 2013 Jerry James <loganjerry@gmail.com> - 0.7.1-4
- Rebuild for coq 8.4pl1
* Thu Dec 13 2012 Jerry James <loganjerry@gmail.com> - 0.7.1-3
- Rebuild for OCaml 4.00.1
* Tue Aug 21 2012 Jerry James <loganjerry@gmail.com> - 0.7.1-2
- Rebuild for coq 8.4
* Mon Jul 30 2012 Jerry James <loganjerry@gmail.com> - 0.7.1-1
- New upstream release
- Install the coq files where coq can find them automatically
* Sun Jul 22 2012 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 0.6.3-6
- Rebuilt for https://fedoraproject.org/wiki/Fedora_18_Mass_Rebuild
* Mon Jan 9 2012 Jerry James <loganjerry@gmail.com> - 0.6.3-5
- Rebuild for OCaml 3.12.1
* Tue Dec 27 2011 Jerry James <loganjerry@gmail.com> - 0.6.3-4
- Rebuild for coq 8.3pl3
* Mon Nov 14 2011 Jerry James <loganjerry@gmail.com> - 0.6.3-3
- Change ExclusiveArch to %%{ocaml_arches}
* Thu Jul 14 2011 Jerry James <loganjerry@gmail.com> - 0.6.3-2
- Move the coq files back to /usr/share to avoid a dependency on coq
- Add paper describing zenon to %%doc
* Tue Jul 12 2011 Jerry James <loganjerry@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@lists.fedoraproject.org> - 0.5.0-8
- Rebuilt for https://fedoraproject.org/wiki/Fedora_15_Mass_Rebuild
* 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
