diff --git a/.gitignore b/.gitignore index 724e07f..fda9400 100644 --- a/.gitignore +++ b/.gitignore @@ -1,2 +1,3 @@ /z3-4.4.0.tar.gz /z3-4.4.1.tar.gz +/z3-4.5.0.tar.gz diff --git a/sources b/sources index 82f3d1b..2963375 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -4336a9df24f090e711c6d42fd4e2b1fc z3-4.4.1.tar.gz +f332befa0d66d81818a06279a0973e25 z3-4.5.0.tar.gz diff --git a/z3-ambiguous-overload.patch b/z3-ambiguous-overload.patch deleted file mode 100644 index 8989e00..0000000 --- a/z3-ambiguous-overload.patch +++ /dev/null @@ -1,23 +0,0 @@ -From 27399309009314f56cdfbd8333f287b1a9b7a3a6 Mon Sep 17 00:00:00 2001 -From: Nuno Lopes -Date: Fri, 27 Nov 2015 12:13:44 +0000 -Subject: [PATCH] fix build with clang - -Signed-off-by: Nuno Lopes ---- - src/util/mpz.cpp | 2 +- - 1 file changed, 1 insertion(+), 1 deletion(-) - -diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp -index 8559279..7dca14b 100644 ---- a/src/util/mpz.cpp -+++ b/src/util/mpz.cpp -@@ -134,7 +134,7 @@ mpz_manager::mpz_manager(): - #endif - - mpz one(1); -- set(m_two64, UINT64_MAX); -+ set(m_two64, (uint64)UINT64_MAX); - add(m_two64, one, m_two64); - } - diff --git a/z3-sse2.patch b/z3-sse2.patch index 3c1dcaa..e7e2aee 100644 --- a/z3-sse2.patch +++ b/z3-sse2.patch @@ -1,20 +1,12 @@ ---- ./src/util/hwf.cpp.orig 2015-10-05 06:07:19.000000000 -0600 -+++ ./src/util/hwf.cpp 2015-10-08 19:57:59.046584973 -0600 -@@ -29,7 +29,7 @@ Revision History: +--- src/util/hwf.cpp.orig 2016-11-07 15:02:30.000000000 -0700 ++++ src/util/hwf.cpp 2016-11-08 21:01:53.533487316 -0700 +@@ -29,8 +29,7 @@ Revision History: #include #endif --#ifndef _M_IA64 -+#ifdef __x86_64 +-#if defined(__x86_64__) || defined(_M_X64) || \ +- defined(__i386) || defined(_M_IX86) ++#if defined(__x86_64__) || defined(_M_X64) #define USE_INTRINSICS #endif -@@ -47,7 +47,7 @@ Revision History: - // Luckily, these are kind of standardized, at least for Windows/Linux/OSX. - #ifdef __clang__ - #undef USE_INTRINSICS --#else -+#elif defined(USE_INTRINSICS) - #include - #endif - diff --git a/z3-stream-bool.patch b/z3-stream-bool.patch deleted file mode 100644 index a4c7c6c..0000000 --- a/z3-stream-bool.patch +++ /dev/null @@ -1,23 +0,0 @@ -From f02d273ee39ae047222e362c37213d29135dc661 Mon Sep 17 00:00:00 2001 -From: Jonathan Wakely -Date: Tue, 2 Feb 2016 23:39:11 +0000 -Subject: [PATCH] Convert stream to bool explicitly - -In C++11 there is no implicit conversion from iostream classes to `void*`, just an explicit conversion to bool. ---- - src/util/debug.cpp | 2 +- - 1 file changed, 1 insertion(+), 1 deletion(-) - -diff --git a/src/util/debug.cpp b/src/util/debug.cpp -index 54c67fe..66676c6 100644 ---- a/src/util/debug.cpp -+++ b/src/util/debug.cpp -@@ -76,7 +76,7 @@ void invoke_gdb() { - for (;;) { - std::cerr << "(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB\n"; - char result; -- bool ok = (std::cin >> result); -+ bool ok = bool(std::cin >> result); - if (!ok) exit(ERR_INTERNAL_FATAL); // happens if std::cin is eof or unattached. - switch(result) { - case 'C': diff --git a/z3.spec b/z3.spec index 13007e2..f9c9f4f 100644 --- a/z3.spec +++ b/z3.spec @@ -4,23 +4,18 @@ # and submit the results upstream, I'm sure many people would be grateful. %global opt %(test -x %{_bindir}/ocamlopt && echo 1 || echo 0) -%global medtag 95c9ccb2959a +%global medtag d57a2a6dce92 Name: z3 -Version: 4.4.1 -Release: 8%{?dist} +Version: 4.5.0 +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 -Source1: %{name}_init.py # Do not try to build with SSE2 on non-x86_64 arches Patch0: %{name}-sse2.patch -# https://github.com/Z3Prover/z3/pull/427 -Patch1: %{name}-stream-bool.patch -# https://github.com/Z3Prover/z3/commit/27399309009314f56cdfbd8333f287b1a9b7a3a6 -Patch2: %{name}-ambiguous-overload.patch BuildRequires: doxygen BuildRequires: gcc-c++ @@ -32,6 +27,7 @@ BuildRequires: ocaml BuildRequires: ocaml-findlib BuildRequires: ocaml-ocamldoc BuildRequires: python2-devel +BuildRequires: python2-setuptools Requires: %{name}-libs%{?_isa} = %{version}-%{release} @@ -96,25 +92,23 @@ Python 2 interface to z3. %prep %setup -q -n %{name}-%{name}-%{version} %patch0 -%patch1 -p1 -%patch2 -p1 # 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, and use an -# soname. +# 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'%{python2_sitearch}/z3'|" \ - -e "s|\(PYTHON_PACKAGE_DIR = \).*|\1'%{buildroot}%{python2_sitearch}/z3'|" \ -e 's/@$(CXX)/$(CXX)/' \ -e 's/ -O3//;s/ -fomit-frame-pointer//' \ - -e "s/@cp /&-p /" \ + -e "s/\(['\"]\)cp\([^[:alnum:]]\)/\1cp -p\2/" \ -e "s/\(SLIBEXTRAFLAGS = '\)'/\1-Wl,--no-whole-archive -Wl,--as-needed'/" \ - -e "s|-shared|& $RPM_LD_FLAGS -Wl,--whole-archive|" \ + -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 '/dllfile/s/\$(SLINK_FLAGS)/& -Wl,-h,lib%{name}.so.0/' \ + -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_64 arches. @@ -123,7 +117,7 @@ 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"),' \ +sed -e 's,\(System\.load\)Library("\(.*\)"),\1("%{_libdir}/z3/\2.so"),' \ -i scripts/update_api.py # Fix character encoding @@ -132,22 +126,25 @@ touch -r RELEASE_NOTES RELEASE_NOTES.utf8 mv -f RELEASE_NOTES.utf8 RELEASE_NOTES # Fix permissions -chmod a-x examples/interp/iz3.cpp find -O3 src -type f -perm /0111 \( -name \*.cpp -o -name \*.h \) \ -exec chmod 0644 {} + -# Fix ocaml documentation generation (broken in 4.4.0) -sed -i 's,api\\html\\ml,api/html/ml,' doc/mk_api_doc.py +# Fix ocaml documentation generation (broken in 4.4.0, broken more in 4.5.0) +sed -e 's,api\\html\\ml,api/html/ml,' \ + -e 's,python/z3.py,python/z3/z3.py,' \ + -e 's,z3enums\.mli,z3enums.ml,' \ + -i doc/mk_api_doc.py %build export CXXFLAGS="$RPM_OPT_FLAGS -fPIC" export LDFLAGS="$RPM_LD_FLAGS -Wl,--as-needed -lgmp" -export LANG="en_US.UTF-8" +export LANG="C.UTF-8" export PYTHON="%{__python2}" # This is NOT an autoconf-generated configure script. -./configure -p %{buildroot}%{_prefix} --githash=%{medtag} --gmp --java --ml -make %{?_smp_mflags} -C build +./configure -p %{_prefix} --githash=%{medtag} --gmp --java --ml +# 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. @@ -164,15 +161,10 @@ pushd doc popd %install -export LANG="en_US.UTF-8" - -# Install the ocaml interface in the right place -sed 's,ocamlfind [[:alpha:]]* ,&-destdir %{buildroot}%{_libdir}/ocaml -ldconf ignore ,' \ - -i build/Makefile +export LANG="C.UTF-8" # Install -mkdir -p %{buildroot}%{python2_sitearch}/%{name} %{buildroot}%{_libdir}/ocaml -make -C build install +make -C build install DESTDIR=%{buildroot} # On 64-bit systems, move the library to the right directory if [ "%{_libdir}" != "%{_prefix}/lib" ]; then @@ -189,15 +181,11 @@ ln -s libz3.so.0 %{buildroot}%{_libdir}/libz3.so mkdir -p %{buildroot}%{_includedir}/%{name} mv %{buildroot}%{_includedir}/*.h %{buildroot}%{_includedir}/%{name} -# Link, rather than copy, the library into the python and ocaml dirs -rm -f %{buildroot}%{python2_sitearch}/%{name}/lib%{name}.so +# Install the python interface +mkdir -p %{buildroot}%{python2_sitearch} +cp -a build/python/%{name} %{buildroot}%{python2_sitearch} ln -s %{_libdir}/lib%{name}.so.0 \ %{buildroot}%{python2_sitearch}/%{name}/lib%{name}.so -rm -f %{buildroot}%{_libdir}/ocaml/Z3/lib%{name}.so -ln -s %{_libdir}/lib%{name}.so.0 %{buildroot}%{_libdir}/ocaml/Z3/lib%{name}.so - -# Add __init__.py for the python module -cp -p %{SOURCE1} %{buildroot}%{python2_sitearch}/%{name}/__init__.py # Move the Java interface to its correct location mkdir -p %{buildroot}%{_libdir}/%{name} @@ -206,10 +194,6 @@ 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} -# Fix permissions -chmod 0755 %{buildroot}%{_bindir}/* %{buildroot}%{_libdir}/*.so.0.0.0 \ - %{buildroot}%{_libdir}/%{name}/*.so - #%%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 @@ -217,7 +201,7 @@ chmod 0755 %{buildroot}%{_bindir}/* %{buildroot}%{_libdir}/*.so.0.0.0 \ # run on the koji builders successfully. If not, the tests will have to be run # manually on machines with more available memory. # -#export LANG="en_US.UTF-8" +#export LANG="C.UTF-8" #pushd build #make test #./test-z3 /a @@ -228,7 +212,7 @@ chmod 0755 %{buildroot}%{_bindir}/* %{buildroot}%{_libdir}/*.so.0.0.0 \ %postun libs -p /sbin/ldconfig %files -%doc README RELEASE_NOTES +%doc README.md RELEASE_NOTES %{_bindir}/%{name} %files libs @@ -250,23 +234,28 @@ chmod 0755 %{buildroot}%{_bindir}/* %{buildroot}%{_libdir}/*.so.0.0.0 \ %files -n ocaml-%{name} %dir %{_libdir}/ocaml/Z3/ %{_libdir}/ocaml/Z3/META -%{_libdir}/ocaml/Z3/*.a %{_libdir}/ocaml/Z3/*.cma %{_libdir}/ocaml/Z3/*.cmi -%{_libdir}/ocaml/Z3/*.cmo -%{_libdir}/ocaml/Z3/*.o +%{_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/*.ml %{_libdir}/ocaml/Z3/*.mli %files -n python-%{name} %{python2_sitearch}/%{name}/ %changelog +* 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. diff --git a/z3_init.py b/z3_init.py deleted file mode 100644 index ae966ed..0000000 --- a/z3_init.py +++ /dev/null @@ -1 +0,0 @@ -from z3 import *