Download raw body.
[update] math/z3: update to 4.13.0
26.08.2024 21:45, Kirill A. Korinsky пишет:
> ports@,
>
> Here an update version of this diff
VERSION is used once and can be inlined.
PKGNAME not needed as DISTNAME is already lowercase.
One patch had offsets (need 'make update-patches') and could be simplified
to make it obviuos what we patch and why.
COMPILER comment does not match -std=gnuc++17 usage.
Upstream has non-empty src/test/ and a default-ON Z3_BUILD_TEST_EXECUTABLES
option, but we still set NO_TEST=Yes -- either don't build or run them.
'make update-plist' changed the @conflict marker (result is the same),
I think we want that, or at least not manually revert it everytime.
MODPY_RUNDEP=No seems missing unless z3 really needs python at runtime.
> On Wed, 21 Aug 2024 00:30:09 +0200,
> Kirill A. Korinsky <kirill@korins.ky> wrote:
>>
>> ports@,
>>
>> Here is a clean update of math/z3 to the latest release.
>>
>> Changelog:
>> https://github.com/Z3Prover/z3/releases/tag/z3-4.13.0
>>
>> Tested on -current/amd64.
>>
>> So the crashing problem is still here, see:
>> https://github.com/Z3Prover/z3/issues/6902
I see three reproducers there that fit into a post-test!
>>
>> But it exists on the current version in ports, which means the update
>> doesn't break anything new.
Which we can use as an argument to not create too much fuzz and leave optimiztions
on until a proper fix shows up; at least I cannot judge at all what impact that has.
>>
>
> After spending some time to dig into the issue which lead to crash, I had
> discovered that such crash doesn't reproduced if I build z3 wihtout
> optimization (-O0).
-O1 also crashes.
>
> During that time I had noticed and fixed a few cases with broken stack...
> Unfortently it doesn't help with the crash.
>
> So, here an updated diff which builds z3 without optimization. It, probably,
> works slower but I can't crash it anymore.
>
> I suggest to keep it that way, until it's fixed.
>
> An updated diff:
New diff including all the feedback above, you can now hack on the port and
iterate over 'make retest' until it no longer crashes (or you give up) ;-)
Index: Makefile
===================================================================
RCS file: /cvs/ports/math/z3/Makefile,v
diff -u -p -r1.33 Makefile
--- Makefile 6 May 2024 12:23:45 -0000 1.33
+++ Makefile 27 Aug 2024 19:58:52 -0000
@@ -1,16 +1,12 @@
COMMENT = Z3 theorem prover
-VERSION = 4.12.2
-REVISION = 1
-
GH_ACCOUNT = Z3Prover
GH_PROJECT = z3
-GH_TAGNAME = ${GH_PROJECT}-${VERSION}
+GH_TAGNAME = ${GH_PROJECT}-4.13.0
DISTNAME = ${GH_TAGNAME}
-PKGNAME = ${DISTNAME:L}
-SHARED_LIBS = z3 4.0 # 4.10
+SHARED_LIBS = z3 4.1
CATEGORIES = math
@@ -19,25 +15,39 @@ WANTLIB += c m pthread ${COMPILER_LIBCXX
# MIT
PERMIT_PACKAGE = Yes
-# c++11
+# C++17
COMPILER = base-clang ports-gcc
MODULES = devel/cmake \
lang/python
-CONFIGURE_ARGS += -DZ3_ENABLE_EXAMPLE_TARGETS=ON \
- -DZ3_INCLUDE_GIT_HASH=OFF \
+MODPY_RUNDEP = No
+
+CONFIGURE_ARGS = -DZ3_BUILD_PYTHON_BINDINGS=ON \
+ -DZ3_ENABLE_EXAMPLE_TARGETS=ON \
-DZ3_INCLUDE_GIT_DESCRIBE=OFF \
- -DZ3_BUILD_PYTHON_BINDINGS=ON \
+ -DZ3_INCLUDE_GIT_HASH=OFF \
-DZ3_USE_LIB_GMP=OFF
DEBUG_PACKAGES = ${BUILD_PACKAGES}
WRKDIST = ${WRKDIR}/z3-${DISTNAME}
-NO_TEST = Yes
+# https://github.com/Z3Prover/z3/issues/6902
+# effectively -O0 to avoid crashes with -O[12]
+MODCMAKE_DEBUG = Yes
pre-configure:
${SUBST_CMD} ${WRKSRC}/scripts/mk_util.py
+
+post-test:
+ # 4.12.2 segfaults on 1,2,3
+ # 4.13.0 segfaults on 2,3 and warns on 1
+.for _repro in \
+ '(declare-datatype)' \
+ '(declare-datatype a)' \
+ '(declare-const p Bool)'
+ -echo ${_repro:Q} | (cd ${WRKBUILD} && ./z3 -in)
+.endfor
.include <bsd.port.mk>
Index: distinfo
===================================================================
RCS file: /cvs/ports/math/z3/distinfo,v
diff -u -p -r1.14 distinfo
--- distinfo 12 Aug 2023 13:31:09 -0000 1.14
+++ distinfo 27 Aug 2024 18:34:26 -0000
@@ -1,2 +1,2 @@
-SHA256 (z3-4.12.2.tar.gz) = n1jzcQvSCUCFlRp1eRVQ9UeQPXX+fi/LNzxfA/x2G48=
-SIZE (z3-4.12.2.tar.gz) = 5401038
+SHA256 (z3-4.13.0.tar.gz) = AbzGHINi43u4n9JDD34zheht95FQGb0s5F3p2b2TRQI=
+SIZE (z3-4.13.0.tar.gz) = 5520232
\ No newline at end of file
Index: patches/patch-cmake_cxx_compiler_flags_overrides_cmake
===================================================================
RCS file: /cvs/ports/math/z3/patches/patch-cmake_cxx_compiler_flags_overrides_cmake,v
diff -u -p -r1.2 patch-cmake_cxx_compiler_flags_overrides_cmake
--- patches/patch-cmake_cxx_compiler_flags_overrides_cmake 11 Mar 2022 19:36:33 -0000 1.2
+++ patches/patch-cmake_cxx_compiler_flags_overrides_cmake 27 Aug 2024 18:38:44 -0000
@@ -1,3 +1,5 @@
+Removed hardcoded optimizations
+
Index: cmake/cxx_compiler_flags_overrides.cmake
--- cmake/cxx_compiler_flags_overrides.cmake.orig
+++ cmake/cxx_compiler_flags_overrides.cmake
Index: patches/patch-scripts_mk_util_py
===================================================================
RCS file: /cvs/ports/math/z3/patches/patch-scripts_mk_util_py,v
diff -u -p -r1.10 patch-scripts_mk_util_py
--- patches/patch-scripts_mk_util_py 9 Feb 2023 06:53:56 -0000 1.10
+++ patches/patch-scripts_mk_util_py 27 Aug 2024 18:42:43 -0000
@@ -1,7 +1,11 @@
+- Remove hardcoded optimizations
+- Fix .so versioning
+- use -fPIC to build shared libs on all archs
+
Index: scripts/mk_util.py
--- scripts/mk_util.py.orig
+++ scripts/mk_util.py
-@@ -2607,7 +2607,6 @@ def mk_config():
+@@ -2609,7 +2609,6 @@ def mk_config():
EXAMP_DEBUG_FLAG = '-g'
CPPFLAGS = '%s -DZ3DEBUG -D_DEBUG' % CPPFLAGS
else:
@@ -9,7 +13,7 @@ Index: scripts/mk_util.py
if GPROF:
CXXFLAGS += '-fomit-frame-pointer'
CPPFLAGS = '%s -DNDEBUG -D_EXTERNAL_RELEASE' % CPPFLAGS
-@@ -2632,7 +2631,7 @@ def mk_config():
+@@ -2634,7 +2633,7 @@ def mk_config():
SO_EXT = '.so'
SLIBFLAGS = '-shared'
elif sysname == 'OpenBSD':
@@ -18,15 +22,12 @@ Index: scripts/mk_util.py
SLIBFLAGS = '-shared'
elif sysname == 'SunOS':
SO_EXT = '.so'
-@@ -2648,9 +2647,8 @@ def mk_config():
+@@ -2650,7 +2649,7 @@ def mk_config():
LIB_EXT = '.lib'
else:
raise MKException('Unsupported platform: %s' % sysname)
- if is64():
-- if not sysname.startswith('CYGWIN') and not sysname.startswith('MSYS') and not sysname.startswith('MINGW'):
-- CXXFLAGS = '%s -fPIC' % CXXFLAGS
-+ if not sysname.startswith('CYGWIN') and not sysname.startswith('MSYS') and not sysname.startswith('MINGW'):
-+ CXXFLAGS = '%s -fPIC' % CXXFLAGS
++ if true:
+ if not sysname.startswith('CYGWIN') and not sysname.startswith('MSYS') and not sysname.startswith('MINGW'):
+ CXXFLAGS = '%s -fPIC' % CXXFLAGS
elif not LINUX_X64:
- CXXFLAGS = '%s -m32' % CXXFLAGS
- LDFLAGS = '%s -m32' % LDFLAGS
Index: pkg/PLIST
===================================================================
RCS file: /cvs/ports/math/z3/pkg/PLIST,v
diff -u -p -r1.9 PLIST
--- pkg/PLIST 11 Mar 2022 19:36:33 -0000 1.9
+++ pkg/PLIST 27 Aug 2024 19:19:02 -0000
@@ -1,4 +1,4 @@
-@conflict py3-z3-solver-*
+@conflict ${MODPY_PY_PREFIX}z3-solver-*
@bin bin/z3
include/z3++.h
include/z3.h
[update] math/z3: update to 4.13.0