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