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 %bcond_with     sse2            # SSE2 instructions
   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
  13 %ifarch %{x8664} x32 pentium4
  14 %define         with_sse2       1
  15 %endif
  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
  19 Name:           z3
  20 Version:        4.12.2
  21 Release:        2
  22 License:        MIT
  23 Group:          Applications/Engineering
  24 #Source0Download: https://github.com/Z3Prover/z3/releases
  25 Source0:        https://github.com/Z3Prover/z3/archive/z3-%{version}.tar.gz
  26 # Source0-md5:  4061317f7948c19abd13041c5a32b057
  27 Patch0:         %{name}-pld.patch
  28 Patch1:         %{name}-sse.patch
  29 Patch2:         %{name}-includes.patch
  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
  40 BuildRequires:  ocaml-zarith-devel
  41 %endif
  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
  49 %description -l pl
  50 Z3 to wydajne narzędzie do dowodzenia twierdzeń tworzone przez
  51 Microsoft Research.
  52
  53 %package devel
  54 Summary:        Development files for Z3
  55 Summary(pl.UTF-8):      Pliki programistyczne Z3
  56 Group:          Development/Libraries
  57 Requires:       %{name} = %{version}-%{release}
  58
  59 %description devel
  60 Development files for Z3.
  61
  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
  69 BuildArch:      noarch
  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}
  94 Requires:       ocaml-zarith
  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}
 110 Requires:       ocaml-zarith-devel
 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
 133 %prep
 134 %setup -q -n z3-z3-%{version}
 135 %patch0 -p1
 136 %patch1 -p1
 137 %patch2 -p1
 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
 143
 144 %build
 145 %if %{with ocaml}
 146 # ml not supported by CMakeLists.txt, need to generate some files
 147 %if %{without ocaml_opt}
 148 # hack to avoid configuration failure
 149 OCAMLOPT=ocamlc \
 150 %endif
 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 .. \
 180         -DCMAKE_INSTALL_INCLUDEDIR=include/z3 \
 181         -DCMAKE_INSTALL_LIBDIR=%{_lib} \
 182         -DCMAKE_INSTALL_PYTHON_PKG_DIR=%{py_sitescriptdir} \
 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 \
 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 \
 191         %{!?with_sse2:-DUSE_SSE2=OFF} \
 192         -DZ3_USE_LIB_GMP=ON
 193
 194 %{__make}
 195
 196 %if %{with ocaml}
 197 # no cmake suite for ocaml; do it manually (basing on Makefile generated by mk_make.py from `configure --ml`)
 198 install -d src/api/ml
 199 cp -p ../build/api/ml/META src/api/ml
 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
 207 cp -p ../src/api/ml/z3.mli src/api/ml/z3.mli
 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
 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
 211 %if %{with ocaml_opt}
 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
 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
 216 ocamlfind ocamlopt -package zarith -linkall -shared -o src/api/ml/z3ml.cmxs -I . -I src/api/ml src/api/ml/z3ml.cmxa
 217 %endif
 218 %endif
 219
 220 %install
 221 rm -rf $RPM_BUILD_ROOT
 222
 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
 229
 230 %if %{with ocaml}
 231 cd build-cmake
 232 install -d $RPM_BUILD_ROOT%{_libdir}/ocaml/stublibs
 233 ocamlfind install -destdir $RPM_BUILD_ROOT%{_libdir}/ocaml Z3 src/api/ml/META \
 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
 240
 241 %{__rm} $RPM_BUILD_ROOT%{_libdir}/ocaml/stublibs/dllz3ml.so.owner
 242 %if %{without ocaml_opt}
 243 %{__sed} -i -e '/archive.*native/d' $RPM_BUILD_ROOT%{_libdir}/ocaml/Z3/META
 244 %endif
 245 cd ..
 246 %endif
 247
 248 install -d $RPM_BUILD_ROOT%{_examplesdir}/%{name}-%{version}
 249 cp -a examples/* $RPM_BUILD_ROOT%{_examplesdir}/%{name}-%{version}
 250
 251 # packaged as %doc in -apidocs
 252 %{__rm} -r $RPM_BUILD_ROOT%{_docdir}/api
 253
 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)
 262 %doc LICENSE.txt README.md RELEASE_NOTES.md
 263 %attr(755,root,root) %{_libdir}/libz3.so.*.*.*.*
 264 %ghost %attr(755,root,root) %{_libdir}/libz3.so.4.12
 265 %attr(755,root,root) %{_bindir}/z3
 266
 267 %files devel
 268 %defattr(644,root,root,755)
 269 %attr(755,root,root) %{_libdir}/libz3.so
 270 %{_includedir}/z3
 271 %{_pkgconfigdir}/z3.pc
 272 %{_libdir}/cmake/z3
 273 %{_examplesdir}/%{name}-%{version}
 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
 292 %{_libdir}/ocaml/Z3/META
 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)
 300 %{_libdir}/ocaml/Z3/libz3ml.a
 301 %{_libdir}/ocaml/Z3/z3*.cmi
 302 %{_libdir}/ocaml/Z3/z3*.mli
 303 %if %{with ocaml_opt}
 304 %{_libdir}/ocaml/Z3/z3ml.a
 305 %{_libdir}/ocaml/Z3/z3*.cmx
 306 %{_libdir}/ocaml/Z3/z3ml.cmxa
 307 %endif
 308 %endif
 309
 310 %files -n python-z3
 311 %defattr(644,root,root,755)
 312 %{py_sitescriptdir}/z3