# 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