%global medtag 3b1b82bef05a Name: z3 Version: 4.8.1 Release: 1%{?dist} Summary: Satisfiability Modulo Theories (SMT) solver License: MIT URL: https://github.com/Z3Prover/z3 Source0: https://github.com/Z3Prover/z3/archive/%{name}-%{version}.tar.gz BuildRequires: doxygen BuildRequires: gcc-c++ BuildRequires: gmp-devel BuildRequires: graphviz BuildRequires: java-devel BuildRequires: jpackage-utils BuildRequires: ocaml BuildRequires: ocaml-findlib BuildRequires: ocaml-ocamldoc BuildRequires: ocaml-num-devel BuildRequires: python3-devel BuildRequires: python3dist(setuptools) Requires: %{name}-libs%{?_isa} = %{version}-%{release} %description Z3 is a satisfiability modulo theories (SMT) solver; given a set of constraints with variables, it reports a set of values for those variables that would meet the constraints. The Z3 input format is an extension of the one defined by the SMT-LIB 2.0 standard. Z3 supports arithmetic, fixed-size bit-vectors, extensional arrays, datatypes, uninterpreted functions, and quantifiers. %package libs Summary: Library for applications that use z3 functionality %description libs Library for applications that use z3 functionality. %package devel Summary: Header files for build applications that use z3 Requires: %{name}-libs%{?_isa} = %{version}-%{release} %description devel Header files for build applications that use z3. %package doc Summary: API documentation for Z3 BuildArch: noarch %description doc API documentation for Z3. %package -n java-%{name} Summary: Java interface to z3 Requires: %{name}-libs%{?_isa} = %{version}-%{release} Requires: java Requires: jpackage-utils %description -n java-%{name} Java interface to z3. %package -n ocaml-%{name} Summary: Ocaml interface to z3 Requires: %{name}-libs%{?_isa} = %{version}-%{release} %description -n ocaml-%{name} Ocaml interface to z3. %package -n ocaml-%{name}-devel Summary: Files for building ocaml applications that use z3 Requires: ocaml-%{name}%{?_isa} = %{version}-%{release} %description -n ocaml-%{name}-devel Files for building ocaml applications that use z3. %package -n python3-%{name} %{?python_provide:%python_provide python3-%{name}} Summary: Python 3 interface to z3 Requires: %{name}-libs%{?_isa} = %{version}-%{release} # This can be removed once Fedora 29 reaches EOL Obsoletes: python2-%{name} < 4.8 Provides: python2-%{name} = 4.8 %description -n python3-%{name} Python 3 interface to z3. %prep %setup -q -n %{name}-%{name}-%{version} # Install python objects into the right place, enable verbose builds, use # Fedora CFLAGS, preserve timestamps when installing, include the entire # contents of the archives in the library, link the library with the correct # flags, don't hide library symbols needed by the executable, use an soname, # and build the ocaml files with debug info. sed -e "s|^\(PYTHON_PACKAGE_DIR=\).*|\1'%{python3_sitearch}'|" \ -e 's/@$(CXX)/$(CXX)/' \ -e '/O3/d' \ -e "s/\(['\"]\)cp\([^[:alnum:]]\)/\1cp -p\2/" \ -e "s/\(SLIBEXTRAFLAGS = '\)'/\1-Wl,--no-whole-archive -Wl,--as-needed'/" \ -e "/SLIBFLAGS/s|-shared|& $RPM_LD_FLAGS -Wl,--whole-archive|" \ -e 's/\(libz3$(SO_EXT)\)\(\\n\)/\1 -Wl,--no-whole-archive\2/' \ -e "s/'tstomp\.cpp',/& '-fPIC',/" \ -e 's/ -fvisibility=hidden//' \ -e '/dll_file/s/\$(SLINK_FLAGS)/& -Wl,-h,lib%{name}.so.0/' \ -e "s/OCAML_FLAGS = ''/OCAML_FLAGS = '-g'/" \ -i scripts/mk_util.py # Do not try to build with SSE2 support on non-x86 arches. %ifnarch %{ix86} x86_64 sed -i 's/exec_compiler_cmd.*-msse.*:/None:/' scripts/mk_util.py %endif # Comply with the Java packaging guidelines sed -e 's,\(System\.load\)Library("\(.*\)"),\1("%{_libdir}/z3/\2.so"),' \ -i scripts/update_api.py # Fix character encoding iconv -f iso8859-1 -t utf-8 RELEASE_NOTES > RELEASE_NOTES.utf8 touch -r RELEASE_NOTES RELEASE_NOTES.utf8 mv -f RELEASE_NOTES.utf8 RELEASE_NOTES # Fix permissions find -O3 src -type f -perm /0111 \( -name \*.cpp -o -name \*.h \) \ -exec chmod 0644 {} + %build export CXXFLAGS="$RPM_OPT_FLAGS -fPIC" export LANG="C.UTF-8" export PYTHON="%{__python3}" # This is NOT an autoconf-generated configure script. ./configure -p %{_prefix} --githash=%{medtag} --gmp --java --ml --python # FIXME: intermittent build failures with %%{?_smp_mflags} make -C build # The z3 binary is NOT linked with libz3, but instead has duplicate copies of a # lot of object files, so rebuild it. But first, add library links. pushd build mv libz3.so libz3.so.0.0.0 ln -s libz3.so.0.0.0 libz3.so.0 ln -s libz3.so.0 libz3.so g++ $RPM_OPT_FLAGS -fopenmp -o z3 shell/*.o $RPM_LD_FLAGS -L. -lz3 -lgmp popd # Build the documentation pushd doc %{__python3} mk_api_doc.py --ml --no-dotnet popd %install export LANG="C.UTF-8" # Install the python3 interface make -C build install DESTDIR=%{buildroot} rm -f %{buildroot}%{python3_sitearch}/%{name}/lib/libz3.so ln -s %{_libdir}/libz3.so.0 %{buildroot}%{python3_sitearch}/%{name}/lib/libz3.so # On 64-bit systems, move the library to the right directory if [ "%{_libdir}" != "%{_prefix}/lib" ]; then mkdir -p %{buildroot}%{_libdir} mv %{buildroot}%{_prefix}/lib/libz3.so* %{buildroot}%{_libdir} fi # Make library links mv %{buildroot}%{_libdir}/libz3.so %{buildroot}%{_libdir}/libz3.so.0.0.0 ln -s libz3.so.0.0.0 %{buildroot}%{_libdir}/libz3.so.0 ln -s libz3.so.0 %{buildroot}%{_libdir}/libz3.so # Move the header files into their own directory mkdir -p %{buildroot}%{_includedir}/%{name} mv %{buildroot}%{_includedir}/*.h %{buildroot}%{_includedir}/%{name} # Move the Java interface to its correct location mkdir -p %{buildroot}%{_libdir}/%{name} mkdir -p %{buildroot}%{_jnidir} mv %{buildroot}%{_prefix}/lib/*.jar %{buildroot}%{_jnidir} ln -s %{_jnidir}/com.microsoft.z3.jar %{buildroot}%{_libdir}/%{name} mv %{buildroot}%{_prefix}/lib/lib%{name}java.so %{buildroot}%{_libdir}/%{name} #%%check # Some of the tests require more memory than the koji builders have available. # However, valgrind also shows a large number of memory leaks. I will work # with upstream to fix the leaks, then try again to see if the tests can be # run on the koji builders successfully. If not, the tests will have to be run # manually on machines with more available memory. # #export LANG="C.UTF-8" #pushd build #make test #./test-z3 /a #popd %files %doc README.md RELEASE_NOTES %{_bindir}/%{name} %files libs %license LICENSE.txt %{_libdir}/lib%{name}.so.* %files devel %{_includedir}/%{name}/ %{_libdir}/lib%{name}.so %files doc %doc doc/api/html examples %license LICENSE.txt %files -n java-%{name} %{_libdir}/%{name}/ %{_jnidir}/com.microsoft.z3.jar %files -n ocaml-%{name} %dir %{_libdir}/ocaml/Z3/ %{_libdir}/ocaml/Z3/META %{_libdir}/ocaml/Z3/*.cma %{_libdir}/ocaml/Z3/*.cmi %{_libdir}/ocaml/Z3/*.cmxs %{_libdir}/ocaml/Z3/*.so %files -n ocaml-%{name}-devel %{_libdir}/ocaml/Z3/*.a %{_libdir}/ocaml/Z3/*.cmx %{_libdir}/ocaml/Z3/*.cmxa %{_libdir}/ocaml/Z3/*.mli %files -n python3-%{name} %{python3_sitearch}/%{name}/ %changelog * Tue Oct 30 2018 Jerry James - 4.8.1-1 - New upstream version - Drop python2 subpackage (bz 1634981) * Fri Sep 7 2018 Jerry James - 4.7.1-5 - Build with SSE2 support on 32-bit x86 * Sat Jul 14 2018 Fedora Release Engineering - 4.7.1-5 - Rebuilt for https://fedoraproject.org/wiki/Fedora_29_Mass_Rebuild * Wed Jul 11 2018 Richard W.M. Jones - 4.7.1-4 - OCaml 4.07.0 (final) rebuild. * Wed Jun 20 2018 Richard W.M. Jones - 4.7.1-3 - OCaml 4.07.0-rc1 rebuild. * Tue Jun 19 2018 Miro Hrončok - 4.7.1-2 - Rebuilt for Python 3.7 * Tue May 22 2018 Jerry James - 4.7.1-1 - New upstream version (bz 1581516) - Drop upstreamed -vector patch * Fri Feb 09 2018 Fedora Release Engineering - 4.6.0-2 - Rebuilt for https://fedoraproject.org/wiki/Fedora_28_Mass_Rebuild * Sun Dec 24 2017 Jerry James - 4.6.0-1 - New upstream version (bz 1527531) - Add a python3 subpackage * Sun Dec 17 2017 Zbigniew Jędrzejewski-Szmek - 4.5.0-8 - Python 2 binary package renamed to python2-z3 See https://fedoraproject.org/wiki/FinalizingFedoraSwitchtoPython3 * Fri Nov 17 2017 Richard W.M. Jones - 4.5.0-7 - OCaml 4.06.0 rebuild. - Add dependency on ocaml-num. * Tue Aug 08 2017 Richard W.M. Jones - 4.5.0-6 - OCaml 4.05.0 rebuild. * Thu Jul 27 2017 Fedora Release Engineering - 4.5.0-5 - Rebuilt for https://fedoraproject.org/wiki/Fedora_27_Mass_Rebuild * Tue Jun 27 2017 Richard W.M. Jones - 4.5.0-4 - OCaml 4.04.2 rebuild. * Fri May 12 2017 Richard W.M. Jones - 4.5.0-3 - OCaml 4.04.1 rebuild. * Sat Feb 11 2017 Fedora Release Engineering - 4.5.0-2 - Rebuilt for https://fedoraproject.org/wiki/Fedora_26_Mass_Rebuild * Tue Nov 8 2016 Jerry James - 4.5.0-1 - New upstream version - All patches except -sse2 have been upstreamed; drop them - Upstream now ships __init__.py; drop our version - Drop all the buildroot tricks; Makefile supports DESTDIR now - Use C.UTF-8 instead of en_US.UTF-8 * Sat Nov 05 2016 Richard W.M. Jones - 4.4.1-8 - Rebuild for OCaml 4.04.0. * Tue Jul 19 2016 Fedora Release Engineering - 4.4.1-7 - https://fedoraproject.org/wiki/Changes/Automatic_Provides_for_Python_RPM_Packages * Wed Jul 13 2016 Jerry James - 4.4.1-6 - Fix Java interface (bz 1353773) * Thu Jun 30 2016 Jerry James - 4.4.1-5 - Fix __init__.py (bz 1351580) * Fri Feb 05 2016 Fedora Release Engineering - 4.4.1-4 - Rebuilt for https://fedoraproject.org/wiki/Fedora_24_Mass_Rebuild * Tue Feb 02 2016 Jonathan Wakely - 4.4.1-3 - Patched for C++11 compatibility. * Wed Jan 20 2016 Jerry James - 4.4.1-2 - Add __init__.py to the python interface (bz 1298429) * Thu Oct 8 2015 Jerry James - 4.4.1-1 - New upstream version * Tue Jul 28 2015 Richard W.M. Jones - 4.4.0-4 - OCaml 4.02.3 rebuild. * Thu Jun 25 2015 Richard W.M. Jones - 4.4.0-3 - ocaml-4.02.2 final rebuild. * Thu Jun 18 2015 Richard W.M. Jones - 4.4.0-2 - ocaml-4.02.2 rebuild. * Wed May 27 2015 Jerry James - 4.4.0-1 - New upstream version * Wed Apr 22 2015 Jerry James - 4.3.2-3.20150329git.29606b5 - Fix issues found on review (bz 1206826) * Mon Mar 30 2015 Jerry James - 4.3.2-2.20150329git.29606b5 - Update to latest git HEAD - Include examples in -doc * Sat Mar 28 2015 Jerry James - 4.3.2-1.20150327git.ac21ffe - Initial RPM