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:        4
  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