packages: LADR/LADR.spec - builds

Wed May 6 16:59:24 CEST 2009

Author: baggins                      Date: Wed May  6 14:59:24 2009 GMT
Module: packages                      Tag: HEAD
---- Log message:
- builds

---- Files affected:
packages/LADR:
   LADR.spec (1.1 -> 1.2) 

---- Diffs:

================================================================
Index: packages/LADR/LADR.spec
diff -u packages/LADR/LADR.spec:1.1 packages/LADR/LADR.spec:1.2

--- packages/LADR/LADR.spec:1.1	Wed May  6 16:22:03 2009
+++ packages/LADR/LADR.spec	Wed May  6 16:59:19 2009
@@ -1,11 +1,15 @@
 # $Revision$, $Date$
+#
+# TODO:
+#	- pl descriptions
+#
 %define	LADRver	2009-02A
 Summary:	Library for Automated Deduction Research
 Name:		LADR
 Version:	%(echo %{LADRver} | tr '-' .)
 Release:	0.1
 License:	GPL v2
-Group:		Applications
+Group:		Libraries
 Source0:	http://www.cs.unm.edu/~mccune/mace4/download/%{name}-%{LADRver}.tar.gz
 # Source0-md5:	f37a5304737ea2b14caf90d0a784964e
 Source1:	%{name}-libtoolize
@@ -14,8 +18,11 @@
 BuildRoot:	%{tmpdir}/%{name}-%{version}-root-%(id -u -n)
 
 %description
-
-%description -l pl.UTF-8
+LADR (Library for Automated Deduction Research) is a library for
+use in constructing theorem provers.  Among other useful routines it
+provides facilities for applying inference rules such as resolution
+and paramodulation to clauses.  LADR is used by the prover9 theorem
+prover, and by the mace4 countermodel generator.
 
 %package devel
 Summary:	Header files for LADR library
@@ -42,13 +49,36 @@
 Statyczna biblioteka LADR.
 
 %package -n prover9
-Summary:	-
-Summary(pl.UTF-8):	-
-Group:		-
+Summary:	Theorem prover and countermodel generator
+Group:		Applications/Science
+Requires:	%{name} = %{version}-%{release}
 
 %description -n prover9
+This package provides the Prover9 resolution/paramodulation theorem
+prover and the Mace4 countermodel generator.
+
+Prover9 is an automated theorem prover for first-order and equational
+logic. It is a successor of the Otter prover.  Prover9 uses the
+inference techniques of ordered resolution and paramodulation with
+literal selection.
+
+The program Mace4 searches for finite structures satisfying first-order
+and equational statements, the same kind of statement that Prover9
+accepts. If the statement is the denial of some conjecture, any
+structures found by Mace4 are counterexamples to the conjecture.
+
+Mace4 can be a valuable complement to Prover9, looking for
+counterexamples before (or at the same time as) using Prover9 to search
+for a proof. It can also be used to help debug input clauses and formulas
+for Prover9.
+
+%package apps
+Summary:	The LADR deduction library, miscellaneous applications
+Group:		Applications/Science
+Requires:	%{name} = %{version}-%{release}
 
-%description -n prover9 -l pl.UTF-8
+%description apps
+This package provides miscellaneous LADR applications.
 
 %prep
 %setup -q -n %{name}-%{LADRver}
@@ -62,8 +92,17 @@
 
 %install
 rm -rf $RPM_BUILD_ROOT
-install -d $RPM_BUILD_ROOT{%{_bindir},%{_libdir},%{_includedir}} \
-	$RPM_BUILD_ROOT%{_examplesdir}/%{name}-%{version}
+install -d $RPM_BUILD_ROOT{%{_bindir},%{_libdir},%{_includedir}/ladr} \
+	$RPM_BUILD_ROOT%{_examplesdir}/prover9-%{version}
+
+cp -a prover9.examples $RPM_BUILD_ROOT%{_examplesdir}/prover9-%{version}
+cp -a mace4.examples $RPM_BUILD_ROOT%{_examplesdir}/prover9-%{version}
+
+install ladr/*.h $RPM_BUILD_ROOT%{_includedir}/ladr
+
+install bin/* $RPM_BUILD_ROOT%{_bindir}
+
+libtool --mode=install --tag=CC cp -a ladr/libladr.la $RPM_BUILD_ROOT%{_libdir}
 
 %clean
 rm -rf $RPM_BUILD_ROOT
@@ -73,14 +112,13 @@
 
 %files
 %defattr(644,root,root,755)
-%doc AUTHORS CREDITS ChangeLog NEWS README THANKS TODO
 %attr(755,root,root) %{_libdir}/libladr.so.*.*
 %attr(755,root,root) %ghost %{_libdir}/libladr.so.4
 
-#%{_examplesdir}/%{name}-%{version}
 
 %files devel
 %defattr(644,root,root,755)
+%doc ladr/html
 %{_includedir}/ladr
 %{_libdir}/libladr.la
 %attr(755,root,root) %{_libdir}/libladr.so
@@ -91,8 +129,46 @@
 
 %files -n prover9
 %defattr(644,root,root,755)
-%attr(755,root,root) %{_bindir}/*
-#%{_datadir}/%{name}-ext
+%attr(755,root,root) %{_bindir}/prover9
+%attr(755,root,root) %{_bindir}/prooftrans
+%attr(755,root,root) %{_bindir}/mace4
+%attr(755,root,root) %{_bindir}/isofilter
+%attr(755,root,root) %{_bindir}/isofilter0
+%attr(755,root,root) %{_bindir}/isofilter2
+%attr(755,root,root) %{_bindir}/interpformat
+%{_examplesdir}/prover9-%{version}
+
+%files apps
+%defattr(644,root,root,755)
+%attr(755,root,root) %{_bindir}/attack
+%attr(755,root,root) %{_bindir}/autosketches4
+%attr(755,root,root) %{_bindir}/clausefilter
+%attr(755,root,root) %{_bindir}/clausetester
+%attr(755,root,root) %{_bindir}/complex
+%attr(755,root,root) %{_bindir}/directproof
+%attr(755,root,root) %{_bindir}/dprofiles
+%attr(755,root,root) %{_bindir}/fof-prover9
+%attr(755,root,root) %{_bindir}/get_givens
+%attr(755,root,root) %{_bindir}/get_interps
+%attr(755,root,root) %{_bindir}/get_kept
+%attr(755,root,root) %{_bindir}/gvizify
+%attr(755,root,root) %{_bindir}/idfilter
+%attr(755,root,root) %{_bindir}/interpfilter
+%attr(755,root,root) %{_bindir}/ladr_to_tptp
+%attr(755,root,root) %{_bindir}/latfilter
+%attr(755,root,root) %{_bindir}/looper
+%attr(755,root,root) %{_bindir}/miniscope
+%attr(755,root,root) %{_bindir}/mirror-flip
+%attr(755,root,root) %{_bindir}/newauto
+%attr(755,root,root) %{_bindir}/newsax
+%attr(755,root,root) %{_bindir}/olfilter
+%attr(755,root,root) %{_bindir}/perm3
+%attr(755,root,root) %{_bindir}/renamer
+%attr(755,root,root) %{_bindir}/rewriter
+%attr(755,root,root) %{_bindir}/sigtest
+%attr(755,root,root) %{_bindir}/tptp_to_ladr
+%attr(755,root,root) %{_bindir}/unfast
+%attr(755,root,root) %{_bindir}/upper-covers
 
 %define date	%(echo `LC_ALL="C" date +"%a %b %d %Y"`)
 %changelog
@@ -100,6 +176,9 @@
 All persons listed below can be reached at <cvs_login>@pld-linux.org
 
 $Log$
+Revision 1.2  2009/05/06 14:59:19  baggins
+- builds
+
 Revision 1.1  2009/05/06 14:22:03  baggins
 - initial revision
 
================================================================

---- CVS-web:
    http://cvs.pld-linux.org/cgi-bin/cvsweb.cgi/packages/LADR/LADR.spec?r1=1.1&r2=1.2&f=u

