]>
Commit | Line | Data |
---|---|---|
79443d4c JB |
1 | # |
2 | # Conditional build: | |
3 | %bcond_without apidocs # Doxygen documentation | |
4 | %bcond_with dotnet # .NET API (requires MS .NET SDK + mono) | |
5 | %bcond_without ocaml # OCaml API | |
6 | %bcond_without ocaml_opt # skip building native optimized binaries (bytecode is always built) | |
45674594 | 7 | %bcond_with sse2 # SSE2 instructions |
79443d4c JB |
8 | |
9 | # not yet available on x32 (ocaml 4.02.1), update when upstream will support it | |
10 | %ifnarch %{ix86} %{x8664} %{arm} aarch64 ppc sparc sparcv9 | |
11 | %undefine with_ocaml_opt | |
12 | %endif | |
45674594 JB |
13 | %ifarch %{x8664} x32 pentium4 |
14 | %define with_sse2 1 | |
15 | %endif | |
79443d4c JB |
16 | |
17 | Summary: High-performance theorem prover developed at Microsoft Research | |
18 | Summary(pl.UTF-8): Wydajne narzędzie do dowodzenia twierdzeń tworzone przez Microsoft Research | |
3cec6e31 | 19 | Name: z3 |
45674594 | 20 | Version: 4.12.2 |
bb2993cf | 21 | Release: 2 |
79443d4c | 22 | License: MIT |
3cec6e31 | 23 | Group: Applications/Engineering |
79443d4c | 24 | #Source0Download: https://github.com/Z3Prover/z3/releases |
01b2836f | 25 | Source0: https://github.com/Z3Prover/z3/archive/z3-%{version}.tar.gz |
45674594 | 26 | # Source0-md5: 4061317f7948c19abd13041c5a32b057 |
79443d4c | 27 | Patch0: %{name}-pld.patch |
45674594 | 28 | Patch1: %{name}-sse.patch |
bb2993cf | 29 | Patch2: %{name}-includes.patch |
79443d4c JB |
30 | URL: https://github.com/Z3Prover/z3 |
31 | BuildRequires: cmake >= 3.4 | |
32 | %{?with_apidocs:BuildRequires: doxygen} | |
33 | BuildRequires: gmp-devel | |
34 | BuildRequires: libgomp-devel | |
35 | BuildRequires: libstdc++-devel >= 6:4.7 | |
36 | %{?with_dotnet:BuildRequires: mono-devel} | |
37 | %if %{with ocaml} | |
38 | BuildRequires: ocaml | |
39 | BuildRequires: ocaml-findlib | |
01b2836f | 40 | BuildRequires: ocaml-zarith-devel |
79443d4c | 41 | %endif |
3cec6e31 JR |
42 | BuildRequires: python |
43 | BuildRoot: %{tmpdir}/%{name}-%{version}-root-%(id -u -n) | |
44 | ||
45 | %description | |
46 | Z3 is a high-performance theorem prover being developed at Microsoft | |
47 | Research. | |
48 | ||
79443d4c JB |
49 | %description -l pl |
50 | Z3 to wydajne narzędzie do dowodzenia twierdzeń tworzone przez | |
51 | Microsoft Research. | |
52 | ||
3cec6e31 JR |
53 | %package devel |
54 | Summary: Development files for Z3 | |
79443d4c | 55 | Summary(pl.UTF-8): Pliki programistyczne Z3 |
3cec6e31 | 56 | Group: Development/Libraries |
79443d4c | 57 | Requires: %{name} = %{version}-%{release} |
3cec6e31 JR |
58 | |
59 | %description devel | |
60 | Development files for Z3. | |
61 | ||
79443d4c JB |
62 | %description devel -l pl.UTF-8 |
63 | Pliki programistyczne Z3. | |
64 | ||
65 | %package apidocs | |
66 | Summary: API documentation for Z3 library | |
67 | Summary(pl.UTF-8): Dokumentacja API Biblioteki Z3 | |
68 | Group: Documentation | |
79443d4c | 69 | BuildArch: noarch |
79443d4c JB |
70 | |
71 | %description apidocs | |
72 | API documentation for Z3 library. | |
73 | ||
74 | %description apidocs -l pl.UTF-8 | |
75 | Dokumentacja API Biblioteki Z3. | |
76 | ||
77 | %package -n java-z3 | |
78 | Summary: Java API for Z3 library | |
79 | Summary(pl.UTF-8): API języka Java do biblioteki Z3 | |
80 | Group: Libraries/Java | |
81 | Requires: %{name} = %{version}-%{release} | |
82 | ||
83 | %description -n java-z3 | |
84 | Java API for Z3 theorem prover library. | |
85 | ||
86 | %description -n java-z3 -l pl.UTF-8 | |
87 | API języka Java do biblioteki dowodzenia twierdzeń Z3. | |
88 | ||
89 | %package -n ocaml-z3 | |
90 | Summary: Z3 binding for OCaml | |
91 | Summary(pl.UTF-8): Wiązania Z3 dla OCamla | |
92 | Group: Libraries | |
93 | Requires: %{name} = %{version}-%{release} | |
01b2836f | 94 | Requires: ocaml-zarith |
79443d4c JB |
95 | %requires_eq ocaml-runtime |
96 | ||
97 | %description -n ocaml-z3 | |
98 | This package contains files needed to run bytecode executables using | |
99 | Z3 library. | |
100 | ||
101 | %description -n ocaml-z3 -l pl.UTF-8 | |
102 | Pakiet ten zawiera binaria potrzebne do uruchamiania programów | |
103 | używających biblioteki Z3. | |
104 | ||
105 | %package -n ocaml-z3-devel | |
106 | Summary: Z3 binding for OCaml - development part | |
107 | Summary(pl.UTF-8): Wiązania Z3 dla OCamla - cześć programistyczna | |
108 | Group: Development/Libraries | |
109 | Requires: ocaml-z3 = %{version}-%{release} | |
01b2836f | 110 | Requires: ocaml-zarith-devel |
79443d4c JB |
111 | %requires_eq ocaml |
112 | ||
113 | %description -n ocaml-z3-devel | |
114 | This package contains files needed to develop OCaml programs using Z3 | |
115 | library. | |
116 | ||
117 | %description -n ocaml-z3-devel -l pl.UTF-8 | |
118 | Pakiet ten zawiera pliki niezbędne do tworzenia programów używających | |
119 | biblioteki Z3. | |
120 | ||
121 | %package -n python-z3 | |
122 | Summary: Python API for Z3 library | |
123 | Summary(pl.UTF-8): API języka Python do biblioteki Z3 | |
124 | Group: Libraries/Python | |
125 | Requires: %{name} = %{version}-%{release} | |
126 | ||
127 | %description -n python-z3 | |
128 | Python API for Z3 theorem prover library. | |
129 | ||
130 | %description -n python-z3 -l pl.UTF-8 | |
131 | API języka Python do biblioteki dowodzenia twierdzeń Z3. | |
132 | ||
3cec6e31 | 133 | %prep |
01b2836f | 134 | %setup -q -n z3-z3-%{version} |
79443d4c | 135 | %patch0 -p1 |
45674594 | 136 | %patch1 -p1 |
bb2993cf | 137 | %patch2 -p1 |
45674594 JB |
138 | |
139 | %if %{without sse2} | |
140 | # no cmake option to disable, just architecture+compiler check | |
141 | %{__sed} -i -e 's/if (HAS_SSE2)/if (FALSE)/' CMakeLists.txt | |
142 | %endif | |
3cec6e31 JR |
143 | |
144 | %build | |
79443d4c JB |
145 | %if %{with ocaml} |
146 | # ml not supported by CMakeLists.txt, need to generate some files | |
5cc33889 JB |
147 | %if %{without ocaml_opt} |
148 | # hack to avoid configuration failure | |
149 | OCAMLOPT=ocamlc \ | |
150 | %endif | |
79443d4c JB |
151 | %{__python} scripts/mk_make.py \ |
152 | --ml | |
153 | # --dotnet --java --python | |
154 | ||
155 | # clean up so that cmake can be run | |
156 | %{__rm} src/ast/pattern/database.h \ | |
157 | src/util/z3_version.h \ | |
158 | $(find src -name '*.hpp') \ | |
159 | src/api/api_commands.cpp \ | |
160 | src/api/api_log_macros.cpp \ | |
161 | src/api/api_log_macros.h \ | |
162 | src/api/dll/gparams_register_modules.cpp \ | |
163 | src/api/dll/install_tactic.cpp \ | |
164 | src/api/dll/mem_initializer.cpp \ | |
165 | src/shell/gparams_register_modules.cpp \ | |
166 | src/shell/install_tactic.cpp \ | |
167 | src/shell/mem_initializer.cpp \ | |
168 | src/test/gparams_register_modules.cpp \ | |
169 | src/test/install_tactic.cpp \ | |
170 | src/test/mem_initializer.cpp | |
171 | %endif | |
172 | ||
173 | # use (unofficial) cmake suite for regular build, because mk_make would | |
174 | # require too much patching to comply with PLD standards (%{_lib}-awareness, | |
175 | # optflags, verbose make...) | |
176 | ||
177 | install -d build-cmake | |
178 | cd build-cmake | |
179 | %cmake .. \ | |
4bf987e0 JB |
180 | -DCMAKE_INSTALL_INCLUDEDIR=include/z3 \ |
181 | -DCMAKE_INSTALL_LIBDIR=%{_lib} \ | |
79443d4c | 182 | -DCMAKE_INSTALL_PYTHON_PKG_DIR=%{py_sitescriptdir} \ |
01b2836f JB |
183 | %{?with_apidocs:-DZ3_BUILD_DOCUMENTATION=ON} \ |
184 | %{?with_dotnet:-DZ3_BUILD_DOTNET_BINDINGS=ON} \ | |
185 | -DZ3_BUILD_JAVA_BINDINGS=ON \ | |
186 | -DZ3_BUILD_LIBZ3_SHARED=ON \ | |
0bc82cec JB |
187 | -DZ3_BUILD_PYTHON_BINDINGS=ON \ |
188 | %{?with_dotnet:-DZ3_INSTALL_DOTNET_BINDINGS=ON} \ | |
189 | -DZ3_INSTALL_JAVA_BINDINGS=ON \ | |
190 | -DZ3_INSTALL_PYTHON_BINDINGS=ON \ | |
45674594 | 191 | %{!?with_sse2:-DUSE_SSE2=OFF} \ |
0bc82cec | 192 | -DZ3_USE_LIB_GMP=ON |
3cec6e31 | 193 | |
3cec6e31 JR |
194 | %{__make} |
195 | ||
79443d4c | 196 | %if %{with ocaml} |
804ec7be | 197 | # no cmake suite for ocaml; do it manually (basing on Makefile generated by mk_make.py from `configure --ml`) |
79443d4c JB |
198 | install -d src/api/ml |
199 | cp -p ../build/api/ml/META src/api/ml | |
01b2836f JB |
200 | ocamlfind ocamlc -package zarith -ccopt "%{rpmcxxflags} -I../src/api -I../src/api/ml -o src/api/ml/z3native_stubs.o" -c ../src/api/ml/z3native_stubs.c |
201 | ocamlfind ocamlc -package zarith -i -I src/api/ml -c ../src/api/ml/z3enums.ml > src/api/ml/z3enums.mli | |
202 | ocamlfind ocamlc -package zarith -I src/api/ml -o src/api/ml/z3enums.cmi -c src/api/ml/z3enums.mli | |
203 | ocamlfind ocamlc -package zarith -I src/api/ml -o src/api/ml/z3enums.cmo -c ../src/api/ml/z3enums.ml | |
204 | ocamlfind ocamlc -package zarith -i -I src/api/ml -o ../src/api/ml/z3native.ml > src/api/ml/z3native.mli | |
205 | ocamlfind ocamlc -package zarith -I src/api/ml -o src/api/ml/z3native.cmi -c src/api/ml/z3native.mli | |
206 | ocamlfind ocamlc -package zarith -I src/api/ml -o src/api/ml/z3native.cmo -c ../src/api/ml/z3native.ml | |
79443d4c | 207 | cp -p ../src/api/ml/z3.mli src/api/ml/z3.mli |
01b2836f JB |
208 | ocamlfind ocamlc -package zarith -I src/api/ml -o src/api/ml/z3.cmi -c src/api/ml/z3.mli |
209 | ocamlfind ocamlc -package zarith -I src/api/ml -o src/api/ml/z3.cmo -c ../src/api/ml/z3.ml | |
804ec7be | 210 | ocamlmklib -o src/api/ml/z3ml -I src/api/ml src/api/ml/z3native_stubs.o src/api/ml/z3enums.cmo src/api/ml/z3native.cmo src/api/ml/z3.cmo -L. -lz3 -cclib -fopenmp |
79443d4c | 211 | %if %{with ocaml_opt} |
01b2836f JB |
212 | ocamlfind ocamlopt -package zarith -I src/api/ml -o src/api/ml/z3enums.cmx -c ../src/api/ml/z3enums.ml |
213 | ocamlfind ocamlopt -package zarith -I src/api/ml -o src/api/ml/z3native.cmx -c ../src/api/ml/z3native.ml | |
214 | ocamlfind ocamlopt -package zarith -I src/api/ml -o src/api/ml/z3.cmx -c ../src/api/ml/z3.ml | |
804ec7be | 215 | ocamlmklib -o src/api/ml/z3ml -I src/api/ml src/api/ml/z3native_stubs.o src/api/ml/z3enums.cmx src/api/ml/z3native.cmx src/api/ml/z3.cmx -L. -lz3 -cclib -fopenmp |
01b2836f | 216 | ocamlfind ocamlopt -package zarith -linkall -shared -o src/api/ml/z3ml.cmxs -I . -I src/api/ml src/api/ml/z3ml.cmxa |
79443d4c JB |
217 | %endif |
218 | %endif | |
219 | ||
3cec6e31 JR |
220 | %install |
221 | rm -rf $RPM_BUILD_ROOT | |
3cec6e31 | 222 | |
79443d4c JB |
223 | %{__make} -C build-cmake install \ |
224 | DESTDIR=$RPM_BUILD_ROOT | |
225 | ||
226 | %py_comp $RPM_BUILD_ROOT%{py_sitescriptdir} | |
227 | %py_ocomp $RPM_BUILD_ROOT%{py_sitescriptdir} | |
228 | %py_postclean | |
3cec6e31 | 229 | |
79443d4c JB |
230 | %if %{with ocaml} |
231 | cd build-cmake | |
68d8dbb4 | 232 | install -d $RPM_BUILD_ROOT%{_libdir}/ocaml/stublibs |
79443d4c | 233 | ocamlfind install -destdir $RPM_BUILD_ROOT%{_libdir}/ocaml Z3 src/api/ml/META \ |
5cc33889 JB |
234 | src/api/ml/z3*.mli src/api/ml/z3*.cmi \ |
235 | src/api/ml/dllz3ml.so src/api/ml/libz3ml.a src/api/ml/z3ml.cma \ | |
236 | %if %{with ocaml_opt} | |
237 | src/api/ml/z3*.cmx \ | |
238 | src/api/ml/z3ml.a src/api/ml/z3ml.cmxa src/api/ml/z3ml.cmxs | |
239 | %endif | |
79443d4c JB |
240 | |
241 | %{__rm} $RPM_BUILD_ROOT%{_libdir}/ocaml/stublibs/dllz3ml.so.owner | |
5cc33889 | 242 | %if %{without ocaml_opt} |
68d8dbb4 | 243 | %{__sed} -i -e '/archive.*native/d' $RPM_BUILD_ROOT%{_libdir}/ocaml/Z3/META |
5cc33889 | 244 | %endif |
79443d4c JB |
245 | cd .. |
246 | %endif | |
247 | ||
248 | install -d $RPM_BUILD_ROOT%{_examplesdir}/%{name}-%{version} | |
3cec6e31 JR |
249 | cp -a examples/* $RPM_BUILD_ROOT%{_examplesdir}/%{name}-%{version} |
250 | ||
79443d4c JB |
251 | # packaged as %doc in -apidocs |
252 | %{__rm} -r $RPM_BUILD_ROOT%{_docdir}/api | |
253 | ||
3cec6e31 JR |
254 | %clean |
255 | rm -rf $RPM_BUILD_ROOT | |
256 | ||
257 | %post -p /sbin/ldconfig | |
258 | %postun -p /sbin/ldconfig | |
259 | ||
260 | %files | |
261 | %defattr(644,root,root,755) | |
45674594 | 262 | %doc LICENSE.txt README.md RELEASE_NOTES.md |
79443d4c | 263 | %attr(755,root,root) %{_libdir}/libz3.so.*.*.*.* |
45674594 | 264 | %ghost %attr(755,root,root) %{_libdir}/libz3.so.4.12 |
79443d4c | 265 | %attr(755,root,root) %{_bindir}/z3 |
3cec6e31 JR |
266 | |
267 | %files devel | |
268 | %defattr(644,root,root,755) | |
3cec6e31 | 269 | %attr(755,root,root) %{_libdir}/libz3.so |
804ec7be JB |
270 | %{_includedir}/z3 |
271 | %{_pkgconfigdir}/z3.pc | |
79443d4c | 272 | %{_libdir}/cmake/z3 |
3cec6e31 | 273 | %{_examplesdir}/%{name}-%{version} |
79443d4c JB |
274 | |
275 | %if %{with apidocs} | |
276 | %files apidocs | |
277 | %defattr(644,root,root,755) | |
278 | %doc build-cmake/doc/api/html/{search,*.{css,html,js,png}} | |
279 | %endif | |
280 | ||
281 | %files -n java-z3 | |
282 | %defattr(644,root,root,755) | |
283 | %attr(755,root,root) %{_libdir}/libz3java.so | |
284 | %{_javadir}/com.microsoft.z3-*.*.*.*.jar | |
285 | %{_javadir}/com.microsoft.z3.jar | |
286 | ||
287 | %if %{with ocaml} | |
288 | %files -n ocaml-z3 | |
289 | %defattr(644,root,root,755) | |
290 | %attr(755,root,root) %{_libdir}/ocaml/stublibs/dllz3ml.so | |
291 | %dir %{_libdir}/ocaml/Z3 | |
a859ebdf | 292 | %{_libdir}/ocaml/Z3/META |
79443d4c JB |
293 | %{_libdir}/ocaml/Z3/z3ml.cma |
294 | %if %{with ocaml_opt} | |
295 | %attr(755,root,root) %{_libdir}/ocaml/Z3/z3ml.cmxs | |
296 | %endif | |
297 | ||
298 | %files -n ocaml-z3-devel | |
299 | %defattr(644,root,root,755) | |
5cc33889 | 300 | %{_libdir}/ocaml/Z3/libz3ml.a |
79443d4c JB |
301 | %{_libdir}/ocaml/Z3/z3*.cmi |
302 | %{_libdir}/ocaml/Z3/z3*.mli | |
303 | %if %{with ocaml_opt} | |
79443d4c JB |
304 | %{_libdir}/ocaml/Z3/z3ml.a |
305 | %{_libdir}/ocaml/Z3/z3*.cmx | |
306 | %{_libdir}/ocaml/Z3/z3ml.cmxa | |
307 | %endif | |
79443d4c JB |
308 | %endif |
309 | ||
310 | %files -n python-z3 | |
311 | %defattr(644,root,root,755) | |
312 | %{py_sitescriptdir}/z3 |