Re: [update] math/z3: update to 4.13.0

On Tue, 27 Aug 2024 21:59:25 +0200,
Klemens Nanni <kn@openbsd.org> wrote:
>
> 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) ;-)
>

Here an updated version based on yours. Changes:
- improved testing to use smt2 models from examples;
- switching to gcc to build it.

By some reason gcc produces z3 which works quite stable.

I suggest to keep it that way.

The diff:

diff --git math/z3/Makefile math/z3/Makefile
index e498cc1fd76..817b6a763de 100644
--- math/z3/Makefile
+++ math/z3/Makefile
@@ -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,31 @@ WANTLIB += c m pthread ${COMPILER_LIBCXX}
# MIT
PERMIT_PACKAGE = Yes

-# c++11
-COMPILER = base-clang ports-gcc
+# C++17, clang lead to segfaults
+# See: https://github.com/Z3Prover/z3/issues/6902
+COMPILER = 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
-
pre-configure:
${SUBST_CMD} ${WRKSRC}/scripts/mk_util.py

+post-test:
+ @find ${WRKSRC}/examples/SMT-LIB2 \
+ -type f -name "*.smt2" \
+ -exec ${WRKBUILD}/z3 {} \;
+
.include <bsd.port.mk>
diff --git math/z3/distinfo math/z3/distinfo
index 369d2943b90..eba5129710c 100644
--- math/z3/distinfo
+++ math/z3/distinfo
@@ -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
diff --git math/z3/patches/patch-cmake_cxx_compiler_flags_overrides_cmake math/z3/patches/patch-cmake_cxx_compiler_flags_overrides_cmake
index e44cf3bdeae..04496bb1443 100644
--- math/z3/patches/patch-cmake_cxx_compiler_flags_overrides_cmake
+++ math/z3/patches/patch-cmake_cxx_compiler_flags_overrides_cmake
@@ -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
diff --git math/z3/patches/patch-scripts_mk_util_py math/z3/patches/patch-scripts_mk_util_py
index c2470b83b54..ce6155a9cad 100644
--- math/z3/patches/patch-scripts_mk_util_py
+++ math/z3/patches/patch-scripts_mk_util_py
@@ -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
diff --git math/z3/pkg/PLIST math/z3/pkg/PLIST
index d152c2d5254..fd2b1201eaa 100644
--- math/z3/pkg/PLIST
+++ math/z3/pkg/PLIST
@@ -1,4 +1,4 @@
-@conflict py3-z3-solver-*
+@conflict ${MODPY_PY_PREFIX}z3-solver-*
@bin bin/z3
include/z3++.h
include/z3.h


--
wbr, Kirill