- builds

Changed files:
    LADR.spec -> 1.2

diff --git a/LADR.spec b/LADR.spec
index 7f393d9155272841a951669d39c7be850b6b2877..63dde3ae784834168e249ab3891018c6b1bbf30b 100644 (file)
--- a/LADR.spec
+++ b/LADR.spec
@@ -1,10 +1,14 @@
+#
+# 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
@@ -13,8 +17,11 @@ BuildRequires:       libtool
 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
@@ -41,13 +48,36 @@ Static LADR library.
 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}
@@ -61,8 +91,17 @@ install %{SOURCE1} Llibtoolize
 
 %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
@@ -72,14 +111,13 @@ rm -rf $RPM_BUILD_ROOT
 
 %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
@@ -90,5 +128,43 @@ rm -rf $RPM_BUILD_ROOT
 
 %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