# 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.6.3
Release:	3%{?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-%{version}.tar.bz2
Source1:	http://focal.inria.fr/zenon/zenlpar07.pdf
Source2:	zenon-tptp-COM003+2.p
Source3:	zenon-tptp-ReadMe
# Basic documentation (man pages). Submitted upstream 2008-07-25:
Source4:	zenon.1
Source5:	zenon-format.5

BuildRequires:	coq
BuildRequires:	ghostscript
BuildRequires:	ImageMagick
BuildRequires:	ocaml

# This should always match the list in the coq spec file.
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} .

%build
# The -libdir argument identifies where to put the coq files.
./configure -prefix %{_prefix} -libdir %{_datadir}/zenon -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/

%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}/zenon
%{_datadir}/zenon
%{_mandir}/man1/*
%{_mandir}/man5/*

%changelog
* 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