LADR.spec

   1 #
   2 # TODO:
   3 #       - pl descriptions
   4 #
   5 %define LADRver 2009-02A
   6 Summary:        Library for Automated Deduction Research
   7 Name:           LADR
   8 Version:        %(echo %{LADRver} | tr '-' .)
   9 Release:        1
  10 License:        GPL v2
  11 Group:          Libraries
  12 Source0:        http://www.cs.unm.edu/~mccune/mace4/download/%{name}-%{LADRver}.tar.gz
  13 # Source0-md5:  f37a5304737ea2b14caf90d0a784964e
  14 Source1:        %{name}-libtoolize
  15 URL:            http://www.cs.unm.edu/~mccune/mace4/
  16 BuildRequires:  libtool
  17 BuildRoot:      %{tmpdir}/%{name}-%{version}-root-%(id -u -n)
  18
  19 %description
  20 LADR (Library for Automated Deduction Research) is a library for
  21 use in constructing theorem provers.  Among other useful routines it
  22 provides facilities for applying inference rules such as resolution
  23 and paramodulation to clauses.  LADR is used by the prover9 theorem
  24 prover, and by the mace4 countermodel generator.
  25
  26 %package devel
  27 Summary:        Header files for LADR library
  28 Summary(pl.UTF-8):      Pliki nagłówkowe biblioteki LADR
  29 Group:          Development/Libraries
  30 Requires:       %{name} = %{version}-%{release}
  31
  32 %description devel
  33 Header files for LADR library.
  34
  35 %description devel -l pl.UTF-8
  36 Pliki nagłówkowe biblioteki LADR.
  37
  38 %package static
  39 Summary:        Static LADR library
  40 Summary(pl.UTF-8):      Statyczna biblioteka LADR
  41 Group:          Development/Libraries
  42 Requires:       %{name}-devel = %{version}-%{release}
  43
  44 %description static
  45 Static LADR library.
  46
  47 %description static -l pl.UTF-8
  48 Statyczna biblioteka LADR.
  49
  50 %package -n prover9
  51 Summary:        Theorem prover and countermodel generator
  52 Group:          Applications/Science
  53 Requires:       %{name} = %{version}-%{release}
  54
  55 %description -n prover9
  56 This package provides the Prover9 resolution/paramodulation theorem
  57 prover and the Mace4 countermodel generator.
  58
  59 Prover9 is an automated theorem prover for first-order and equational
  60 logic. It is a successor of the Otter prover.  Prover9 uses the
  61 inference techniques of ordered resolution and paramodulation with
  62 literal selection.
  63
  64 The program Mace4 searches for finite structures satisfying first-order
  65 and equational statements, the same kind of statement that Prover9
  66 accepts. If the statement is the denial of some conjecture, any
  67 structures found by Mace4 are counterexamples to the conjecture.
  68
  69 Mace4 can be a valuable complement to Prover9, looking for
  70 counterexamples before (or at the same time as) using Prover9 to search
  71 for a proof. It can also be used to help debug input clauses and formulas
  72 for Prover9.
  73
  74 %package apps
  75 Summary:        The LADR deduction library, miscellaneous applications
  76 Group:          Applications/Science
  77 Requires:       %{name} = %{version}-%{release}
  78
  79 %description apps
  80 This package provides miscellaneous LADR applications.
  81
  82 %prep
  83 %setup -q -n %{name}-%{LADRver}
  84 sed 's|/usr/lib|%{_libdir}|g' %{SOURCE1} > Llibtoolize
  85 chmod 755 Llibtoolize
  86 ./Llibtoolize --patch .
  87
  88 %build
  89 %{__make} all \
  90         CFLAGS="%{rpmcflags}" \
  91         LDFLAGS="%{rpmldflags}"
  92
  93 %install
  94 rm -rf $RPM_BUILD_ROOT
  95 install -d $RPM_BUILD_ROOT{%{_bindir},%{_libdir},%{_includedir}/ladr} \
  96         $RPM_BUILD_ROOT%{_examplesdir}/prover9-%{version}
  97
  98 cp -a prover9.examples $RPM_BUILD_ROOT%{_examplesdir}/prover9-%{version}
  99 cp -a mace4.examples $RPM_BUILD_ROOT%{_examplesdir}/prover9-%{version}
 100
 101 install ladr/*.h $RPM_BUILD_ROOT%{_includedir}/ladr
 102
 103 install bin/* $RPM_BUILD_ROOT%{_bindir}
 104
 105 libtool --mode=install --tag=CC cp -a ladr/libladr.la $RPM_BUILD_ROOT%{_libdir}
 106
 107 %clean
 108 rm -rf $RPM_BUILD_ROOT
 109
 110 %post   -p /sbin/ldconfig
 111 %postun -p /sbin/ldconfig
 112
 113 %files
 114 %defattr(644,root,root,755)
 115 %attr(755,root,root) %{_libdir}/libladr.so.*.*
 116 %attr(755,root,root) %ghost %{_libdir}/libladr.so.4
 117
 118
 119 %files devel
 120 %defattr(644,root,root,755)
 121 %doc ladr/html
 122 %{_includedir}/ladr
 123 %{_libdir}/libladr.la
 124 %attr(755,root,root) %{_libdir}/libladr.so
 125
 126 %files static
 127 %defattr(644,root,root,755)
 128 %{_libdir}/libladr.a
 129
 130 %files -n prover9
 131 %defattr(644,root,root,755)
 132 %attr(755,root,root) %{_bindir}/prover9
 133 %attr(755,root,root) %{_bindir}/prooftrans
 134 %attr(755,root,root) %{_bindir}/mace4
 135 %attr(755,root,root) %{_bindir}/isofilter
 136 %attr(755,root,root) %{_bindir}/isofilter0
 137 %attr(755,root,root) %{_bindir}/isofilter2
 138 %attr(755,root,root) %{_bindir}/interpformat
 139 %{_examplesdir}/prover9-%{version}
 140
 141 %files apps
 142 %defattr(644,root,root,755)
 143 %attr(755,root,root) %{_bindir}/attack
 144 %attr(755,root,root) %{_bindir}/autosketches4
 145 %attr(755,root,root) %{_bindir}/clausefilter
 146 %attr(755,root,root) %{_bindir}/clausetester
 147 %attr(755,root,root) %{_bindir}/complex
 148 %attr(755,root,root) %{_bindir}/directproof
 149 %attr(755,root,root) %{_bindir}/dprofiles
 150 %attr(755,root,root) %{_bindir}/fof-prover9
 151 %attr(755,root,root) %{_bindir}/get_givens
 152 %attr(755,root,root) %{_bindir}/get_interps
 153 %attr(755,root,root) %{_bindir}/get_kept
 154 %attr(755,root,root) %{_bindir}/gvizify
 155 %attr(755,root,root) %{_bindir}/idfilter
 156 %attr(755,root,root) %{_bindir}/interpfilter
 157 %attr(755,root,root) %{_bindir}/ladr_to_tptp
 158 %attr(755,root,root) %{_bindir}/latfilter
 159 %attr(755,root,root) %{_bindir}/looper
 160 %attr(755,root,root) %{_bindir}/miniscope
 161 %attr(755,root,root) %{_bindir}/mirror-flip
 162 %attr(755,root,root) %{_bindir}/newauto
 163 %attr(755,root,root) %{_bindir}/newsax
 164 %attr(755,root,root) %{_bindir}/olfilter
 165 %attr(755,root,root) %{_bindir}/perm3
 166 %attr(755,root,root) %{_bindir}/renamer
 167 %attr(755,root,root) %{_bindir}/rewriter
 168 %attr(755,root,root) %{_bindir}/sigtest
 169 %attr(755,root,root) %{_bindir}/tptp_to_ladr
 170 %attr(755,root,root) %{_bindir}/unfast
 171 %attr(755,root,root) %{_bindir}/upper-covers