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