]>
Commit | Line | Data |
---|---|---|
e3a065a3 JR |
1 | # |
2 | # TODO: | |
3 | # - pl descriptions | |
4 | # | |
1d72af26 JR |
5 | %define LADRver 2009-02A |
6 | Summary: Library for Automated Deduction Research | |
7 | Name: LADR | |
8 | Version: %(echo %{LADRver} | tr '-' .) | |
8efa7b41 | 9 | Release: 1 |
1d72af26 | 10 | License: GPL v2 |
e3a065a3 | 11 | Group: Libraries |
1d72af26 JR |
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 | |
e3a065a3 JR |
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. | |
1d72af26 JR |
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 | |
e3a065a3 JR |
51 | Summary: Theorem prover and countermodel generator |
52 | Group: Applications/Science | |
53 | Requires: %{name} = %{version}-%{release} | |
1d72af26 JR |
54 | |
55 | %description -n prover9 | |
e3a065a3 JR |
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} | |
1d72af26 | 78 | |
e3a065a3 JR |
79 | %description apps |
80 | This package provides miscellaneous LADR applications. | |
1d72af26 JR |
81 | |
82 | %prep | |
83 | %setup -q -n %{name}-%{LADRver} | |
8efa7b41 JR |
84 | sed 's|/usr/lib|%{_libdir}|g' %{SOURCE1} > Llibtoolize |
85 | chmod 755 Llibtoolize | |
1d72af26 JR |
86 | ./Llibtoolize --patch . |
87 | ||
88 | %build | |
23bcb520 | 89 | %{__make} -j1 all \ |
1d72af26 JR |
90 | CFLAGS="%{rpmcflags}" \ |
91 | LDFLAGS="%{rpmldflags}" | |
92 | ||
93 | %install | |
94 | rm -rf $RPM_BUILD_ROOT | |
e3a065a3 JR |
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} | |
1d72af26 JR |
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) | |
1d72af26 JR |
115 | %attr(755,root,root) %{_libdir}/libladr.so.*.* |
116 | %attr(755,root,root) %ghost %{_libdir}/libladr.so.4 | |
117 | ||
1d72af26 JR |
118 | |
119 | %files devel | |
120 | %defattr(644,root,root,755) | |
e3a065a3 | 121 | %doc ladr/html |
1d72af26 JR |
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) | |
e3a065a3 JR |
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 |