Hello community, here is the log from the commit of package z3 for openSUSE:Factory checked in at 2018-03-24 16:16:08 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Comparing /work/SRC/openSUSE:Factory/z3 (Old) and /work/SRC/openSUSE:Factory/.z3.new (New) ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Package is "z3" Sat Mar 24 16:16:08 2018 rev:12 rq:590550 version:4.6.0+git.20180112 Changes: -------- --- /work/SRC/openSUSE:Factory/z3/z3.changes 2017-12-22 12:21:38.275607183 +0100 +++ /work/SRC/openSUSE:Factory/.z3.new/z3.changes 2018-03-24 16:16:18.913475011 +0100 @@ -1,0 +2,58 @@ +Thu Mar 22 19:11:04 UTC 2018 - [email protected] + +- Fix python packaging: create python3-z3 on SLE/Leap 15.0 and + Tumbleweed, and python-z3 on older distros. + +------------------------------------------------------------------- +Tue Jan 16 08:35:11 UTC 2018 - [email protected] + +- Update to version 4.6.0+git.20180112: + * add missing interpreted tail during bottom-up simplification #1452 + * Added apply_result::as_expr to the C++ API. Requested here: https://stackoverflow.com/questions/48071840/get-result-of-tactics-application-as-an-expression-in-z3 + * to ascii or not to ascii #1447 + * fix build + * avoid reset_error in dec_ref in bv_val #1443. Add BSD required template instance #1444 + * make linear search the default for theory_str + * [CMake] Fix #1437. + * Use noreturn attribute and __declspec version. + * revert use of [[noreturn]]. It's not fully supported on compilers #1435 + * add noreturn attribute #1435 + * raise_exception: Annotate that this doesn't return. + * Remove unnecessary copy of coeff in iteration. + * Remove ignored const qualifiers. + * Fix code formatting: Incorrect indentation. + * fix #1429 + * print_stat_f: Remove implicit conversion of float to double. + * Typo fixes. + * set default rewriter behavior in incremental mode to distribute multiplication over addition #1373 + * removing axiom exposing unsoundness, replace by weaker axiom + * add shorthand for translating models #1407 + * add __copy__, __deepcopy__ as alias to translate on same context #1427. Add generalized Gaussian elimination as an option to first-pass NL solver + * fix build of test + * adding pre-processing to nlsat for equations + * fix get-objectives error #1419 message (get-objectives) + * initialize additional assumptions after setup_context is called the first time + * alternate strategies for QF_NIA + * remove custom exception, perhaps this handles exception issue + * add virtual destructor to see if this helps ASan error + * Allowing slices and negative index in assertions + * add Python facility for int2bv, fix #1398 + * Documentation fixes. + * Bumped version number. + * Updated release notes + * add back missing initialization of lo + * fix nlsat regression + * avoid crash on nl + * fix crashes in nlsat + * fix crashes in nlsat + * remove comment out + * add integer branch and bound to nlsat + * small improvements to QF_NIA tactic + * fixes compilation flags for OCaml plugins + +------------------------------------------------------------------- +Mon Jan 15 15:09:28 UTC 2018 - [email protected] + +- Look for python3_sitelib in tumbleweed + +------------------------------------------------------------------- Old: ---- z3-4.5.0+git.20171213.tar.xz New: ---- z3-4.6.0+git.20180112.tar.xz ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Other differences: ------------------ ++++++ z3.spec ++++++ --- /var/tmp/diff_new_pack.Pvt9Du/_old 2018-03-24 16:16:20.257426565 +0100 +++ /var/tmp/diff_new_pack.Pvt9Du/_new 2018-03-24 16:16:20.261426421 +0100 @@ -1,7 +1,7 @@ # # spec file for package z3 # -# Copyright (c) 2017 SUSE LINUX GmbH, Nuernberg, Germany. +# Copyright (c) 2018 SUSE LINUX GmbH, Nuernberg, Germany. # # All modifications and additions to the file contributed by third parties # remain the property of their copyright owners, unless otherwise agreed @@ -16,23 +16,31 @@ # -%define version_unconverted 4.5.0+git.20171213 +%define version_unconverted 4.6.0+git.20180112 %define sover 4_6 - +%if 0%{?suse_version} >= 1500 +# Use python3 n SLE/Leap 15.0 and Tumbleweed +%define _python python3 +%define _python_sitelib %{python3_sitelib} +%else +%define _python python +%define _python_sitelib %{python_sitelib} +# USe python2 on older distros +%endif Name: z3 -Version: 4.5.0+git.20171213 +Version: 4.6.0+git.20180112 Release: 0 Summary: Theorem prover from Microsoft Research License: MIT Group: Productivity/Scientific/Other -Url: https://github.com/Z3Prover/z3/wiki +URL: https://github.com/Z3Prover/z3/wiki Source0: %{name}-%{version}.tar.xz Patch0: remove-timestamp.patch +BuildRequires: %{_python}-devel BuildRequires: cmake BuildRequires: gcc-c++ BuildRequires: gmp-devel BuildRequires: ninja -BuildRequires: python-devel BuildRequires: xz %description @@ -58,16 +66,16 @@ Requires: libz3-%{sover} = %{version} %description devel -Developmnet files for the Z3 library. +Development files for the Z3 library. -%package -n python-%{name} +%package -n %{_python}-%{name} Summary: Python bindings for Z3 Group: Development/Languages/Python Requires: %{name} = %{version} -Provides: %{name}-python = %{version} -Obsoletes: %{name}-python < %{version} +Provides: %{name}-%{_python} = %{version} +Obsoletes: %{name}-%{_python} < %{version} -%description -n python-%{name} +%description -n %{_python}-%{name} Python bindings for the Z3 library. %prep @@ -76,12 +84,13 @@ %build %define __builder ninja -python contrib/cmake/bootstrap.py create +%{_python} contrib/cmake/bootstrap.py create %cmake \ -DBUILD_LIBZ3_SHARED=true \ -DUSE_LIB_GMP=true \ -DBUILD_PYTHON_BINDINGS=true \ -DINSTALL_PYTHON_BINDINGS=true \ + -DPYTHON_EXECUTABLE=%{_bindir}/%{_python} \ -DENABLE_EXAMPLE_TARGETS=false %make_jobs @@ -93,7 +102,8 @@ %files %defattr(-,root,root) -%doc LICENSE.txt README.md RELEASE_NOTES +%license LICENSE.txt +%doc README.md RELEASE_NOTES %{_bindir}/z3 %files -n libz3-%{sover} @@ -108,9 +118,9 @@ %{_libdir}/cmake/z3/Z3Config.cmake %{_libdir}/cmake/z3/Z3Targets* -%files -n python-%{name} +%files -n %{_python}-%{name} %defattr(-,root,root) -%dir %{python_sitelib}/%{name} -%{python_sitelib}/%{name}/*py +%dir %{_python_sitelib}/%{name} +%{_python_sitelib}/%{name}/*py %changelog ++++++ _service ++++++ --- /var/tmp/diff_new_pack.Pvt9Du/_old 2018-03-24 16:16:20.293425267 +0100 +++ /var/tmp/diff_new_pack.Pvt9Du/_new 2018-03-24 16:16:20.297425123 +0100 @@ -4,7 +4,9 @@ <param name="scm">git</param> <param name="changesgenerate">enable</param> <param name="filename">z3</param> - <param name="versionformat">4.5.0+git.%cd</param> + <param name="versionformat">@PARENT_TAG@+git.%cd</param> + <param name="versionrewrite-pattern">z3(.*)</param> + <param name="versionrewrite-replacement">\1</param> </service> <service mode="disabled" name="recompress"> <param name="file">*.tar</param> ++++++ _servicedata ++++++ --- /var/tmp/diff_new_pack.Pvt9Du/_old 2018-03-24 16:16:20.361422816 +0100 +++ /var/tmp/diff_new_pack.Pvt9Du/_new 2018-03-24 16:16:20.361422816 +0100 @@ -1,4 +1,4 @@ <servicedata> <service name="tar_scm"> <param name="url">git://github.com/Z3Prover/z3.git</param> - <param name="changesrevision">387e984bd39a8a6ed636b0210bce6fef79b51bc5</param></service></servicedata> \ No newline at end of file + <param name="changesrevision">450f3c9b459d128135abb5bbd4fa0508fe26bfae</param></service></servicedata> \ No newline at end of file ++++++ z3-4.5.0+git.20171213.tar.xz -> z3-4.6.0+git.20180112.tar.xz ++++++ ++++ 4157 lines of diff (skipped)
