Re: [update] math/z3: update to 4.13.0
03.09.2024 19:07, Kirill A. Korinsky пишет: > Here an updated diff where I've backported patch from upstream which fixed > crash on OpenBSD as side effect. Thanks, committed.
Re: [update] math/z3: update to 4.13.0
On Sat, 31 Aug 2024 21:08:15 +0200,
Klemens Nanni wrote:
>
> You're right, :Q remained from an earlier iteration.
> I dropped it, yielding correct commands now, thanks.
>
Here an updated diff where I've backported patch from upstream which fixed
crash on OpenBSD as side effect.
I also drop testing of crash because
- '(declare-datatype)' and '(declare-datatype a)' doesn't work on 4.13 and
simple complains as:
(error "line 1 column 18: unexpected token used as datatype name")
(error "line 1 column 20: invalid datatype declaration, '(' expected got a")
- '(declare-const p Bool) because this case is covered by example models.
So, finally a diff which works without crash on -current/amd64:
Index: Makefile
===
RCS file: /cvs/ports/math/z3/Makefile,v
retrieving revision 1.33
diff -u -p -r1.33 Makefile
--- Makefile6 May 2024 12:23:45 - 1.33
+++ Makefile3 Sep 2024 16:05:14 -
@@ -1,16 +1,9 @@
COMMENT = Z3 theorem prover
-VERSION = 4.12.2
-REVISION = 1
+DIST_TUPLE = github Z3Proverz3 z3-4.13.0 .
+PKGNAME = ${DISTNAME:S/z3-//}
-GH_ACCOUNT = Z3Prover
-GH_PROJECT = z3
-GH_TAGNAME = ${GH_PROJECT}-${VERSION}
-
-DISTNAME = ${GH_TAGNAME}
-PKGNAME = ${DISTNAME:L}
-
-SHARED_LIBS = z3 4.0 # 4.10
+SHARED_LIBS = z3 4.11
CATEGORIES = math
@@ -19,25 +12,27 @@ 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 \
+MODPY_RUNDEP = No
+
+CONFIGURE_ARGS = -DZ3_BUILD_PYTHON_BINDINGS=ON \
+ -DZ3_ENABLE_EXAMPLE_TARGETS=OFF \
-DZ3_INCLUDE_GIT_HASH=OFF \
- -DZ3_INCLUDE_GIT_DESCRIBE=OFF \
- -DZ3_BUILD_PYTHON_BINDINGS=ON \
-DZ3_USE_LIB_GMP=OFF
DEBUG_PACKAGES = ${BUILD_PACKAGES}
-WRKDIST = ${WRKDIR}/z3-${DISTNAME}
-
-NO_TEST = Yes
-
-pre-configure:
+post-extract:
${SUBST_CMD} ${WRKSRC}/scripts/mk_util.py
+
+post-test:
+ cd ${WRKBUILD} && \
+ find ${WRKSRC}/examples/SMT-LIB2/ -type f -name '*.smt2' \
+ -exec echo \; -print -exec ./z3 {} \;
.include
Index: distinfo
===
RCS file: /cvs/ports/math/z3/distinfo,v
retrieving revision 1.14
diff -u -p -r1.14 distinfo
--- distinfo12 Aug 2023 13:31:09 - 1.14
+++ distinfo3 Sep 2024 16:05:14 -
@@ -1,2 +1,2 @@
-SHA256 (z3-4.12.2.tar.gz) = n1jzcQvSCUCFlRp1eRVQ9UeQPXX+fi/LNzxfA/x2G48=
-SIZE (z3-4.12.2.tar.gz) = 5401038
+SHA256 (Z3Prover-z3-z3-4.13.0.tar.gz) =
AbzGHINi43u4n9JDD34zheht95FQGb0s5F3p2b2TRQI=
+SIZE (Z3Prover-z3-z3-4.13.0.tar.gz) = 5520232
Index: patches/patch-cmake_cxx_compiler_flags_overrides_cmake
===
RCS file:
/cvs/ports/math/z3/patches/patch-cmake_cxx_compiler_flags_overrides_cmake,v
retrieving revision 1.2
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 - 1.2
+++ patches/patch-cmake_cxx_compiler_flags_overrides_cmake 3 Sep 2024
16:05:14 -
@@ -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
retrieving revision 1.10
diff -u -p -r1.10 patch-scripts_mk_util_py
--- patches/patch-scripts_mk_util_py9 Feb 2023 06:53:56 - 1.10
+++ patches/patch-scripts_mk_util_py3 Sep 2024 16:05:14 -
@@ -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
Re: [update] math/z3: update to 4.13.0
31.08.2024 18:10, Kirill A. Korinsky пишет: > not sure that this :Q is required. If I run it with :Q z3 complains as: > > (error "line 1 column 1: unexpected character") > (error "line 1 column 19: unexpected token used as datatype name") > (error "line 1 column 20: unexpected character") > > because it makes a command line like: > > echo \'\(declare-datatype\)\' | > > which produces an invalid input for z3. You're right, :Q remained from an earlier iteration. I dropped it, yielding correct commands now, thanks.
Re: [update] math/z3: update to 4.13.0
On Sat, 31 Aug 2024 16:03:30 +0200,
Klemens Nanni wrote:
>
> 31.08.2024 16:35, Klemens Nanni пишет:
> > 30.08.2024 22:17, Kirill A. Korinsky пишет:
> >> On Tue, 27 Aug 2024 21:59:25 +0200,
> >> Klemens Nanni 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;
> >
> > Sounds good. Do those strictly supersede the reproducers from the issue,
> > or would it make sense to run both in post-test?
> >
Yes, they are. They crashed z3 which is built by clang with the same stacktrace.
> > I also noticed that our -DZ3_ENABLE_EXAMPLE_TARGETS=ON is already the
> > default
> > and =OFF results in less targets being built without PLIST change or effect
> > on your tests, so I think we can spare a few cycles and avoid building
> > whatever isn't used, anyway.
> >
> > Plus, -DZ3_INCLUDE_GIT_HASH=OFF implies -DZ3_INCLUDE_GIT_DESCRIBE=OFF, so
> > the latter can be dropped as well.
> >
> >> By some reason gcc produces z3 which works quite stable.
> >
> > Switching COMPILER makes /usr/src/lib/check_sym report removal of
> > dynamically
> > exported symbols, so a major bump to 5.0 would be in order.
> >
> > Good find, perhaps we can narrow it down further!
> >
Quite possible that this is triggered by clang bug similar to
https://github.com/llvm/llvm-project/issues/55844
> +.for _repro in \
> +'(declare-datatype)' \
> +'(declare-datatype a)' \
> +'(declare-const p Bool)'
> + -echo ${_repro:Q} | (cd ${WRKBUILD} && ./z3 -in)
not sure that this :Q is required. If I run it with :Q z3 complains as:
(error "line 1 column 1: unexpected character")
(error "line 1 column 19: unexpected token used as datatype name")
(error "line 1 column 20: unexpected character")
because it makes a command line like:
echo \'\(declare-datatype\)\' |
which produces an invalid input for z3.
--
wbr, Kirill
Re: [update] math/z3: update to 4.13.0
31.08.2024 16:35, Klemens Nanni пишет:
> 30.08.2024 22:17, Kirill A. Korinsky пишет:
>> On Tue, 27 Aug 2024 21:59:25 +0200,
>> Klemens Nanni 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;
>
> Sounds good. Do those strictly supersede the reproducers from the issue,
> or would it make sense to run both in post-test?
>
> I also noticed that our -DZ3_ENABLE_EXAMPLE_TARGETS=ON is already the default
> and =OFF results in less targets being built without PLIST change or effect
> on your tests, so I think we can spare a few cycles and avoid building
> whatever isn't used, anyway.
>
> Plus, -DZ3_INCLUDE_GIT_HASH=OFF implies -DZ3_INCLUDE_GIT_DESCRIBE=OFF, so
> the latter can be dropped as well.
>
>> By some reason gcc produces z3 which works quite stable.
>
> Switching COMPILER makes /usr/src/lib/check_sym report removal of dynamically
> exported symbols, so a major bump to 5.0 would be in order.
>
> Good find, perhaps we can narrow it down further!
>
>> I suggest to keep it that way.
>
> For your example tests: post-test runs in the ports dir, so you should ensure
> that z3 runs somewhere, where _pbuild is allowed to dump core.
>
> update-patches regen'ed a file and update-plist added some python dir
> after we dropped the RDEP on it -- unimportant changes really, but always
> good to rerun those targets to avoid churn.
>
>
> I'll soon commit with those tweaks, unless someone objects.
Oops, update-patches churn was actually picking up SUBST_CMD changes.
To fix, I moved that into post-extract, such that it runs before patch.
I also switched to DIST_TUPLE for brevity, WRKDIST can thus be dropped, too.
> -+SO_EXT = '.so.${LIBz3_VERSION}'
> ++SO_EXT = '.so.4.1'
Index: Makefile
===
RCS file: /cvs/ports/math/z3/Makefile,v
diff -u -p -r1.33 Makefile
--- Makefile6 May 2024 12:23:45 - 1.33
+++ Makefile31 Aug 2024 14:03:10 -
@@ -1,16 +1,9 @@
COMMENT = Z3 theorem prover
-VERSION = 4.12.2
-REVISION = 1
+DIST_TUPLE = github Z3Proverz3 z3-4.13.0 .
+PKGNAME = ${DISTNAME:S/z3-//}
-GH_ACCOUNT = Z3Prover
-GH_PROJECT = z3
-GH_TAGNAME = ${GH_PROJECT}-${VERSION}
-
-DISTNAME = ${GH_TAGNAME}
-PKGNAME = ${DISTNAME:L}
-
-SHARED_LIBS = z3 4.0 # 4.10
+SHARED_LIBS = z3 5.0
CATEGORIES = math
@@ -19,25 +12,39 @@ WANTLIB += c m pthread ${COMPILER_LIBCXX
# MIT
PERMIT_PACKAGE = Yes
-# c++11
-COMPILER = base-clang ports-gcc
+# C++17, clang leads 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 \
+MODPY_RUNDEP = No
+
+CONFIGURE_ARGS = -DZ3_BUILD_PYTHON_BINDINGS=ON \
+ -DZ3_ENABLE_EXAMPLE_TARGETS=OFF \
-DZ3_INCLUDE_GIT_HASH=OFF \
- -DZ3_INCLUDE_GIT_DESCRIBE=OFF \
- -DZ3_BUILD_PYTHON_BINDINGS=ON \
-DZ3_USE_LIB_GMP=OFF
DEBUG_PACKAGES = ${BUILD_PACKAGES}
-WRKDIST = ${WRKDIR}/z3-${DISTNAME}
-
-NO_TEST = Yes
-
-pre-configure:
+post-extract:
${SUBST_CMD} ${WRKSRC}/scripts/mk_util.py
+
+post-test:
+ # with clang:
+ # 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)
+ @echo
+.endfor
+ # run example models for good measure as well
+ cd ${WRKBUILD} && \
+ find ${WRKSRC}/examples/SMT-LIB2/ -type f -name '*.smt2' \
+ -exec echo \; -print -exec ./z3 {} \;
.include
Index: distinfo
===
RCS file: /cvs/ports/math/z3/distinfo,v
diff -u -p -r1.14 distinfo
--- distinfo12 Aug 2023 13:31:09 - 1.14
+++ distinfo31 Aug 2024 13:54:29 -
@@ -1,2 +1,2 @@
-SHA256 (z3-4.12.2.tar.gz) = n1jzcQvSCUCFlRp1eRVQ9UeQPXX+fi/LNzxfA/x2G48=
-SIZE (z3-4.12.2.tar.gz) = 5401038
+SHA256 (Z3Prover-z3-z3-4.13.0.tar.gz) =
AbzGHINi43u4n9JDD34zheht95FQGb0s5F3p2b2TRQI=
+SIZE (Z3Prover-z3-z3-4.13.0.tar.gz) = 5520232
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 - 1.2
Re: [update] math/z3: update to 4.13.0
30.08.2024 22:17, Kirill A. Korinsky пишет:
> On Tue, 27 Aug 2024 21:59:25 +0200,
> Klemens Nanni 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;
Sounds good. Do those strictly supersede the reproducers from the issue,
or would it make sense to run both in post-test?
I also noticed that our -DZ3_ENABLE_EXAMPLE_TARGETS=ON is already the default
and =OFF results in less targets being built without PLIST change or effect
on your tests, so I think we can spare a few cycles and avoid building
whatever isn't used, anyway.
Plus, -DZ3_INCLUDE_GIT_HASH=OFF implies -DZ3_INCLUDE_GIT_DESCRIBE=OFF, so
the latter can be dropped as well.
> By some reason gcc produces z3 which works quite stable.
Switching COMPILER makes /usr/src/lib/check_sym report removal of dynamically
exported symbols, so a major bump to 5.0 would be in order.
Good find, perhaps we can narrow it down further!
> I suggest to keep it that way.
For your example tests: post-test runs in the ports dir, so you should ensure
that z3 runs somewhere, where _pbuild is allowed to dump core.
update-patches regen'ed a file and update-plist added some python dir
after we dropped the RDEP on it -- unimportant changes really, but always
good to rerun those targets to avoid churn.
I'll soon commit with those tweaks, unless someone objects.
Index: Makefile
===
RCS file: /cvs/ports/math/z3/Makefile,v
diff -u -p -r1.33 Makefile
--- Makefile6 May 2024 12:23:45 - 1.33
+++ Makefile31 Aug 2024 13:34:39 -
@@ -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 5.0
CATEGORIES = math
@@ -19,25 +15,41 @@ WANTLIB += c m pthread ${COMPILER_LIBCXX
# MIT
PERMIT_PACKAGE = Yes
-# c++11
-COMPILER = base-clang ports-gcc
+# C++17, clang leads 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 \
+MODPY_RUNDEP = No
+
+CONFIGURE_ARGS = -DZ3_BUILD_PYTHON_BINDINGS=ON \
+ -DZ3_ENABLE_EXAMPLE_TARGETS=OFF \
-DZ3_INCLUDE_GIT_HASH=OFF \
- -DZ3_INCLUDE_GIT_DESCRIBE=OFF \
- -DZ3_BUILD_PYTHON_BINDINGS=ON \
-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:
+ # with clang:
+ # 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)
+ @echo
+.endfor
+ # run example models for good measure as well
+ cd ${WRKBUILD} && \
+ find ${WRKSRC}/examples/SMT-LIB2/ -type f -name '*.smt2' \
+ -exec echo \; -print -exec ./z3 {} \;
.include
Index: distinfo
===
RCS file: /cvs/ports/math/z3/distinfo,v
diff -u -p -r1.14 distinfo
--- distinfo12 Aug 2023 13:31:09 - 1.14
+++ distinfo30 Aug 2024 21:28:52 -
@@ -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 - 1.2
+++ patches/patch-cmake_cxx_compiler_flags_overrides_cmake 30 Aug 2024
21:28:52 -
@@ -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
Re: [update] math/z3: update to 4.13.0
On Tue, 27 Aug 2024 21:59:25 +0200,
Klemens Nanni 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
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
-
Re: [update] math/z3: update to 4.13.0
Klemens,
Thanks for review and tweak of the diff.
On Tue, 27 Aug 2024 21:59:25 +0200,
Klemens Nanni wrote:
>
> MODPY_RUNDEP=No seems missing unless z3 really needs python at runtime.
>
It has python binding and python API, and can be used from python. Not sure
that it justify it.
> >>
> >> 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.
>
Frankly speaking z3 is quite unstable right now.
For example a build with -O0 crashes at different place (upstream issue is
updated) on trivial theorem:
(declare-const x Int)
(declare-const y Int)
(assert (> (+ (mod x 4) (* 3 (div y 2))) (- x y)))
(check-sat)
but if I rewrite it into python API, it works:
~ $ python3
Python 3.11.9 (main, Aug 14 2024, 08:01:59) [Clang 16.0.6 ] on openbsd7
Type "help", "copyright", "credits" or "license" for more information.
>>> from z3 import *
>>> x, y = Ints('x y')
>>> s = Solver()
>>> s.add((x % 4) + 3 * (y / 2) > x - y)
>>> print(s.sexpr())
(declare-fun y () Int)
(declare-fun x () Int)
(assert (> (+ (mod x 4) (* 3 (div y 2))) (- x y)))
>>>
my point: -O0 make it unstable but usefull, with any optimization it useless.
--
wbr, Kirill
Re: [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 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
--- Makefile6 May 2024 12:23:45 - 1.33
+++ Makefile27 Aug 2024 19:58:52 -
@@ -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
Index: distinfo
===
RCS file: /cvs/ports/math/z3/distinfo,v
diff -u -p -r1.14 distinfo
--- distinfo12 Aug 2023 13:31:09 - 1.14
+++ distinfo27 Aug 2024 18:34:26 -
@@ -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 - 1.2
+++ patches/patch-cmake_cxx_compiler_flags_overrides_cmake 27 Aug 2024
18:38:44 -
@@ -1,3 +1,5 @@
+Removed hardcoded optim
Re: [update] math/z3: update to 4.13.0
On Mon, 26 Aug 2024 21:36:45 +0200, A Tammy wrote: > > > > 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). > > > This sounds like a bug worthy of telling upstream about. > > It was reported to upstream almost year ago [1] but it was closed without fix. So, I have no better solution here. Footnotes: [1] https://github.com/Z3Prover/z3/issues/6902 -- wbr, Kirill
Re: [update] math/z3: update to 4.13.0
On 8/26/24 2:45 PM, Kirill A. Korinsky wrote:
> ports@,
>
> Here an update version of this diff
>
> On Wed, 21 Aug 2024 00:30:09 +0200,
> Kirill A. Korinsky 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
>>
>> But it exists on the current version in ports, which means the update
>> doesn't break anything new.
>>
> 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).
This sounds like a bug worthy of telling upstream about.
> 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:
>
> diff --git math/z3/Makefile math/z3/Makefile
> index e498cc1fd76..5aa42b953cc 100644
> --- math/z3/Makefile
> +++ math/z3/Makefile
> @@ -1,7 +1,6 @@
> COMMENT =Z3 theorem prover
>
> -VERSION =4.12.2
> -REVISION = 1
> +VERSION =4.13.0
>
> GH_ACCOUNT = Z3Prover
> GH_PROJECT = z3
> @@ -10,7 +9,7 @@ GH_TAGNAME = ${GH_PROJECT}-${VERSION}
> DISTNAME = ${GH_TAGNAME}
> PKGNAME =${DISTNAME:L}
>
> -SHARED_LIBS =z3 4.0 # 4.10
> +SHARED_LIBS =z3 4.1 # 4.13
>
> CATEGORIES = math
>
> @@ -31,6 +30,10 @@ CONFIGURE_ARGS += -DZ3_ENABLE_EXAMPLE_TARGETS=ON \
> -DZ3_BUILD_PYTHON_BINDINGS=ON \
> -DZ3_USE_LIB_GMP=OFF
>
> +# Debug build, optimized build crashes
> +# See: https://github.com/Z3Prover/z3/issues/6902
> +MODCMAKE_DEBUG = Yes
> +
> DEBUG_PACKAGES = ${BUILD_PACKAGES}
>
> WRKDIST =${WRKDIR}/z3-${DISTNAME}
> diff --git math/z3/distinfo math/z3/distinfo
> index 369d2943b90..22c9ca84d8a 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
>
>
Re: [update] math/z3: update to 4.13.0
ports@,
Here an update version of this diff
On Wed, 21 Aug 2024 00:30:09 +0200,
Kirill A. Korinsky 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
>
> But it exists on the current version in ports, which means the update
> doesn't break anything new.
>
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).
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:
diff --git math/z3/Makefile math/z3/Makefile
index e498cc1fd76..5aa42b953cc 100644
--- math/z3/Makefile
+++ math/z3/Makefile
@@ -1,7 +1,6 @@
COMMENT = Z3 theorem prover
-VERSION = 4.12.2
-REVISION = 1
+VERSION = 4.13.0
GH_ACCOUNT = Z3Prover
GH_PROJECT = z3
@@ -10,7 +9,7 @@ GH_TAGNAME = ${GH_PROJECT}-${VERSION}
DISTNAME = ${GH_TAGNAME}
PKGNAME = ${DISTNAME:L}
-SHARED_LIBS = z3 4.0 # 4.10
+SHARED_LIBS = z3 4.1 # 4.13
CATEGORIES = math
@@ -31,6 +30,10 @@ CONFIGURE_ARGS +=-DZ3_ENABLE_EXAMPLE_TARGETS=ON \
-DZ3_BUILD_PYTHON_BINDINGS=ON \
-DZ3_USE_LIB_GMP=OFF
+# Debug build, optimized build crashes
+# See: https://github.com/Z3Prover/z3/issues/6902
+MODCMAKE_DEBUG = Yes
+
DEBUG_PACKAGES = ${BUILD_PACKAGES}
WRKDIST = ${WRKDIR}/z3-${DISTNAME}
diff --git math/z3/distinfo math/z3/distinfo
index 369d2943b90..22c9ca84d8a 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
--
wbr, Kirill
[update] math/z3: update to 4.13.0
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
But it exists on the current version in ports, which means the update
doesn't break anything new.
The diff:
diff --git math/z3/Makefile math/z3/Makefile
index e498cc1fd76..723a501406b 100644
--- math/z3/Makefile
+++ math/z3/Makefile
@@ -1,7 +1,6 @@
COMMENT = Z3 theorem prover
-VERSION = 4.12.2
-REVISION = 1
+VERSION = 4.13.0
GH_ACCOUNT = Z3Prover
GH_PROJECT = z3
@@ -10,7 +9,7 @@ GH_TAGNAME = ${GH_PROJECT}-${VERSION}
DISTNAME = ${GH_TAGNAME}
PKGNAME = ${DISTNAME:L}
-SHARED_LIBS = z3 4.0 # 4.10
+SHARED_LIBS = z3 4.1 # 4.13
CATEGORIES = math
diff --git math/z3/distinfo math/z3/distinfo
index 369d2943b90..22c9ca84d8a 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
--
wbr, Kirill
Re: [UPDATE] math/z3 to 4.8.16
Frederic Cambus wrote:
> Hi ports@,
>
> Here is a diff to update z3 to 4.8.16.
>
> Some functions have been removed from the library, so a major bump
> is needed.
>
> Comments? OK?
ok op@
I somehow managed to boostrap F* with OCaml using the updated z3. It's
still half broken (not the parts that deal with z3) and the other half
requires ugly hacks to work. But it verified the hello world so z3 is
fine :)
> Index: Makefile
> ===
> RCS file: /cvs/ports/math/z3/Makefile,v
> retrieving revision 1.25
> diff -u -p -r1.25 Makefile
> --- Makefile 11 Mar 2022 19:36:33 - 1.25
> +++ Makefile 3 May 2022 15:16:12 -
> @@ -1,6 +1,6 @@
> COMMENT =Z3 theorem prover
>
> -VERSION =4.8.9
> +VERSION =4.8.16
>
> GH_ACCOUNT = Z3Prover
> GH_PROJECT = z3
> @@ -8,9 +8,8 @@ GH_TAGNAME = ${GH_PROJECT}-${VERSION}
>
> DISTNAME = ${GH_TAGNAME}
> PKGNAME =${DISTNAME:L}
> -REVISION = 0
>
> -SHARED_LIBS =z3 2.2 # 4.8
> +SHARED_LIBS =z3 3.0 # 4.8
>
> CATEGORIES = math
>
> Index: distinfo
> ===
> RCS file: /cvs/ports/math/z3/distinfo,v
> retrieving revision 1.9
> diff -u -p -r1.9 distinfo
> --- distinfo 18 Sep 2020 07:52:58 - 1.9
> +++ distinfo 3 May 2022 15:16:12 -
> @@ -1,2 +1,2 @@
> -SHA256 (z3-4.8.9.tar.gz) = yf0EubM750//qsPsK8LDINGkzDLjlSA8VRJrEqFP8/Q=
> -SIZE (z3-4.8.9.tar.gz) = 4624159
> +SHA256 (z3-4.8.16.tar.gz) = dfleCfPzX+90blcdXsiKTvuifxvI8aDvERcWdIbsPcY=
> +SIZE (z3-4.8.16.tar.gz) = 5223980
> Index: patches/patch-scripts_mk_util_py
> ===
> RCS file: /cvs/ports/math/z3/patches/patch-scripts_mk_util_py,v
> retrieving revision 1.7
> diff -u -p -r1.7 patch-scripts_mk_util_py
> --- patches/patch-scripts_mk_util_py 11 Mar 2022 19:36:33 - 1.7
> +++ patches/patch-scripts_mk_util_py 3 May 2022 15:16:12 -
> @@ -1,7 +1,7 @@
> Index: scripts/mk_util.py
> --- scripts/mk_util.py.orig
> +++ scripts/mk_util.py
> -@@ -2478,7 +2478,6 @@ def mk_config():
> +@@ -2573,7 +2573,6 @@ def mk_config():
> EXAMP_DEBUG_FLAG = '-g'
> CPPFLAGS = '%s -DZ3DEBUG -D_DEBUG' % CPPFLAGS
> else:
> @@ -9,7 +9,7 @@ Index: scripts/mk_util.py
> if GPROF:
> CXXFLAGS += '-fomit-frame-pointer'
> CPPFLAGS = '%s -DNDEBUG -D_EXTERNAL_RELEASE' % CPPFLAGS
> -@@ -2491,7 +2490,7 @@ def mk_config():
> +@@ -2586,7 +2585,7 @@ def mk_config():
> elif sysname == 'Linux':
> CXXFLAGS = '%s -D_LINUX_' % CXXFLAGS
> OS_DEFINES = '-D_LINUX_'
> @@ -18,7 +18,7 @@ Index: scripts/mk_util.py
> SLIBFLAGS = '-shared'
> SLIBEXTRAFLAGS = '%s -Wl,-soname,libz3.so' % SLIBEXTRAFLAGS
> elif sysname == 'GNU':
> -@@ -2528,9 +2527,9 @@ def mk_config():
> +@@ -2629,9 +2628,9 @@ def mk_config():
> LIB_EXT= '.lib'
> else:
> raise MKException('Unsupported platform: %s' % sysname)
[UPDATE] math/z3 to 4.8.16
Hi ports@,
Here is a diff to update z3 to 4.8.16.
Some functions have been removed from the library, so a major bump
is needed.
Comments? OK?
Index: Makefile
===
RCS file: /cvs/ports/math/z3/Makefile,v
retrieving revision 1.25
diff -u -p -r1.25 Makefile
--- Makefile11 Mar 2022 19:36:33 - 1.25
+++ Makefile3 May 2022 15:16:12 -
@@ -1,6 +1,6 @@
COMMENT = Z3 theorem prover
-VERSION = 4.8.9
+VERSION = 4.8.16
GH_ACCOUNT = Z3Prover
GH_PROJECT = z3
@@ -8,9 +8,8 @@ GH_TAGNAME =${GH_PROJECT}-${VERSION}
DISTNAME = ${GH_TAGNAME}
PKGNAME = ${DISTNAME:L}
-REVISION = 0
-SHARED_LIBS = z3 2.2 # 4.8
+SHARED_LIBS = z3 3.0 # 4.8
CATEGORIES = math
Index: distinfo
===
RCS file: /cvs/ports/math/z3/distinfo,v
retrieving revision 1.9
diff -u -p -r1.9 distinfo
--- distinfo18 Sep 2020 07:52:58 - 1.9
+++ distinfo3 May 2022 15:16:12 -
@@ -1,2 +1,2 @@
-SHA256 (z3-4.8.9.tar.gz) = yf0EubM750//qsPsK8LDINGkzDLjlSA8VRJrEqFP8/Q=
-SIZE (z3-4.8.9.tar.gz) = 4624159
+SHA256 (z3-4.8.16.tar.gz) = dfleCfPzX+90blcdXsiKTvuifxvI8aDvERcWdIbsPcY=
+SIZE (z3-4.8.16.tar.gz) = 5223980
Index: patches/patch-scripts_mk_util_py
===
RCS file: /cvs/ports/math/z3/patches/patch-scripts_mk_util_py,v
retrieving revision 1.7
diff -u -p -r1.7 patch-scripts_mk_util_py
--- patches/patch-scripts_mk_util_py11 Mar 2022 19:36:33 - 1.7
+++ patches/patch-scripts_mk_util_py3 May 2022 15:16:12 -
@@ -1,7 +1,7 @@
Index: scripts/mk_util.py
--- scripts/mk_util.py.orig
+++ scripts/mk_util.py
-@@ -2478,7 +2478,6 @@ def mk_config():
+@@ -2573,7 +2573,6 @@ def mk_config():
EXAMP_DEBUG_FLAG = '-g'
CPPFLAGS = '%s -DZ3DEBUG -D_DEBUG' % CPPFLAGS
else:
@@ -9,7 +9,7 @@ Index: scripts/mk_util.py
if GPROF:
CXXFLAGS += '-fomit-frame-pointer'
CPPFLAGS = '%s -DNDEBUG -D_EXTERNAL_RELEASE' % CPPFLAGS
-@@ -2491,7 +2490,7 @@ def mk_config():
+@@ -2586,7 +2585,7 @@ def mk_config():
elif sysname == 'Linux':
CXXFLAGS = '%s -D_LINUX_' % CXXFLAGS
OS_DEFINES = '-D_LINUX_'
@@ -18,7 +18,7 @@ Index: scripts/mk_util.py
SLIBFLAGS = '-shared'
SLIBEXTRAFLAGS = '%s -Wl,-soname,libz3.so' % SLIBEXTRAFLAGS
elif sysname == 'GNU':
-@@ -2528,9 +2527,9 @@ def mk_config():
+@@ -2629,9 +2628,9 @@ def mk_config():
LIB_EXT= '.lib'
else:
raise MKException('Unsupported platform: %s' % sysname)
Re: [Update] math/z3 : Update to 4.8.6
On Wed Oct 16, 2019 at 02:59:32AM +, wen heping wrote:
> Hi,ports@:
>
>Here is a patch for math/z3 to update to 4.8.6.
>It build well and run well on amd64-current system.
>It defines NO_TEST and no other ports depend on it.
>
> Comments? OK?
> wen
OK rsadowski@
> Index: Makefile
> ===
> RCS file: /cvs/ports/math/z3/Makefile,v
> retrieving revision 1.17
> diff -u -p -r1.17 Makefile
> --- Makefile 12 Jul 2019 20:47:47 - 1.17
> +++ Makefile 16 Oct 2019 02:55:38 -
> @@ -2,15 +2,14 @@
>
> COMMENT =Z3 theorem prover
>
> -VERSION =4.8.5
> +VERSION =4.8.6
>
> GH_ACCOUNT = Z3Prover
> GH_PROJECT = z3
> -GH_TAGNAME = ${GH_PROJECT:U}-${VERSION}
> +GH_TAGNAME = ${GH_PROJECT}-${VERSION}
>
> DISTNAME = ${GH_TAGNAME}
> PKGNAME =${DISTNAME:L}
> -REVISION = 0
>
> SHARED_LIBS =z3 2.0 # 4.8
>
> Index: distinfo
> ===
> RCS file: /cvs/ports/math/z3/distinfo,v
> retrieving revision 1.6
> diff -u -p -r1.6 distinfo
> --- distinfo 5 Jun 2019 05:44:54 - 1.6
> +++ distinfo 16 Oct 2019 02:55:38 -
> @@ -1,2 +1,2 @@
> -SHA256 (Z3-4.8.5.tar.gz) = To4jKIfd+mQ622ow3NN0PLL6ZZFzX70wK0n3AozcA2M=
> -SIZE (Z3-4.8.5.tar.gz) = 4177051
> +SHA256 (z3-4.8.6.tar.gz) = N5IvpQhRcMrWUESY2XWPtjxh1ctbaGicEabF6E8DEbM=
> +SIZE (z3-4.8.6.tar.gz) = 4328752
> Index: patches/patch-scripts_mk_util_py
> ===
> RCS file: /cvs/ports/math/z3/patches/patch-scripts_mk_util_py,v
> retrieving revision 1.3
> diff -u -p -r1.3 patch-scripts_mk_util_py
> --- patches/patch-scripts_mk_util_py 3 Mar 2019 09:16:17 - 1.3
> +++ patches/patch-scripts_mk_util_py 16 Oct 2019 02:55:38 -
> @@ -1,18 +1,9 @@
> -$OpenBSD: patch-scripts_mk_util_py,v 1.3 2019/03/03 09:16:17 rsadowski Exp $
> +$OpenBSD$
>
> Index: scripts/mk_util.py
> --- scripts/mk_util.py.orig
> +++ scripts/mk_util.py
> -@@ -50,7 +50,7 @@ C_COMPILERS=['gcc', 'clang']
> - CSC_COMPILERS=['csc', 'mcs']
> - JAVAC=None
> - JAR=None
> --PYTHON_PACKAGE_DIR=distutils.sysconfig.get_python_lib()
> -+PYTHON_PACKAGE_DIR=distutils.sysconfig.get_python_lib(prefix=getenv("LOCALBASE",
> None))
> - BUILD_DIR='build'
> - REV_BUILD_DIR='..'
> - SRC_DIR='src'
> -@@ -2801,7 +2801,6 @@ def mk_config():
> +@@ -2538,7 +2538,6 @@ def mk_config():
> EXAMP_DEBUG_FLAG = '-g'
> CPPFLAGS = '%s -DZ3DEBUG -D_DEBUG' % CPPFLAGS
> else:
> @@ -20,16 +11,16 @@ Index: scripts/mk_util.py
> if GPROF:
> CXXFLAGS += '-fomit-frame-pointer'
> CPPFLAGS = '%s -DNDEBUG -D_EXTERNAL_RELEASE' % CPPFLAGS
> -@@ -2836,7 +2835,7 @@ def mk_config():
> - elif sysname == 'OpenBSD':
> - CXXFLAGS = '%s -D_OPENBSD_' % CXXFLAGS
> - OS_DEFINES = '-D_OPENBSD_'
> +@@ -2551,7 +2550,7 @@ def mk_config():
> + elif sysname == 'Linux':
> + CXXFLAGS = '%s -D_LINUX_' % CXXFLAGS
> + OS_DEFINES = '-D_LINUX_'
> -SO_EXT = '.so'
> +SO_EXT = '.so.${LIBz3_VERSION}'
> SLIBFLAGS = '-shared'
> - elif sysname.startswith('CYGWIN'):
> - CXXFLAGS = '%s -D_CYGWIN' % CXXFLAGS
> -@@ -2852,9 +2851,9 @@ def mk_config():
> + SLIBEXTRAFLAGS = '%s -Wl,-soname,libz3.so' % SLIBEXTRAFLAGS
> + elif sysname == 'FreeBSD':
> +@@ -2583,9 +2582,9 @@ def mk_config():
> LIB_EXT= '.lib'
> else:
> raise MKException('Unsupported platform: %s' % sysname)
> Index: pkg/PLIST
> ===
> RCS file: /cvs/ports/math/z3/pkg/PLIST,v
> retrieving revision 1.5
> diff -u -p -r1.5 PLIST
> --- pkg/PLIST 3 Mar 2019 09:16:17 - 1.5
> +++ pkg/PLIST 16 Oct 2019 02:55:38 -
> @@ -17,6 +17,7 @@ include/z3_version.h
> lib/cmake/
> lib/cmake/z3/
> lib/cmake/z3/Z3Config.cmake
> +lib/cmake/z3/Z3ConfigVersion.cmake
> lib/cmake/z3/Z3Targets${MODCMAKE_BUILD_SUFFIX}
> lib/cmake/z3/Z3Targets.cmake
> @lib lib/libz3.so.${LIBz3_VERSION}
[Update] math/z3 : Update to 4.8.6
Hi,ports@:
Here is a patch for math/z3 to update to 4.8.6.
It build well and run well on amd64-current system.
It defines NO_TEST and no other ports depend on it.
Comments? OK?
wen
Index: Makefile
===
RCS file: /cvs/ports/math/z3/Makefile,v
retrieving revision 1.17
diff -u -p -r1.17 Makefile
--- Makefile12 Jul 2019 20:47:47 - 1.17
+++ Makefile16 Oct 2019 02:55:38 -
@@ -2,15 +2,14 @@
COMMENT = Z3 theorem prover
-VERSION = 4.8.5
+VERSION = 4.8.6
GH_ACCOUNT = Z3Prover
GH_PROJECT = z3
-GH_TAGNAME = ${GH_PROJECT:U}-${VERSION}
+GH_TAGNAME = ${GH_PROJECT}-${VERSION}
DISTNAME = ${GH_TAGNAME}
PKGNAME = ${DISTNAME:L}
-REVISION = 0
SHARED_LIBS = z3 2.0 # 4.8
Index: distinfo
===
RCS file: /cvs/ports/math/z3/distinfo,v
retrieving revision 1.6
diff -u -p -r1.6 distinfo
--- distinfo5 Jun 2019 05:44:54 - 1.6
+++ distinfo16 Oct 2019 02:55:38 -
@@ -1,2 +1,2 @@
-SHA256 (Z3-4.8.5.tar.gz) = To4jKIfd+mQ622ow3NN0PLL6ZZFzX70wK0n3AozcA2M=
-SIZE (Z3-4.8.5.tar.gz) = 4177051
+SHA256 (z3-4.8.6.tar.gz) = N5IvpQhRcMrWUESY2XWPtjxh1ctbaGicEabF6E8DEbM=
+SIZE (z3-4.8.6.tar.gz) = 4328752
Index: patches/patch-scripts_mk_util_py
===
RCS file: /cvs/ports/math/z3/patches/patch-scripts_mk_util_py,v
retrieving revision 1.3
diff -u -p -r1.3 patch-scripts_mk_util_py
--- patches/patch-scripts_mk_util_py3 Mar 2019 09:16:17 - 1.3
+++ patches/patch-scripts_mk_util_py16 Oct 2019 02:55:38 -
@@ -1,18 +1,9 @@
-$OpenBSD: patch-scripts_mk_util_py,v 1.3 2019/03/03 09:16:17 rsadowski Exp $
+$OpenBSD$
Index: scripts/mk_util.py
--- scripts/mk_util.py.orig
+++ scripts/mk_util.py
-@@ -50,7 +50,7 @@ C_COMPILERS=['gcc', 'clang']
- CSC_COMPILERS=['csc', 'mcs']
- JAVAC=None
- JAR=None
--PYTHON_PACKAGE_DIR=distutils.sysconfig.get_python_lib()
-+PYTHON_PACKAGE_DIR=distutils.sysconfig.get_python_lib(prefix=getenv("LOCALBASE",
None))
- BUILD_DIR='build'
- REV_BUILD_DIR='..'
- SRC_DIR='src'
-@@ -2801,7 +2801,6 @@ def mk_config():
+@@ -2538,7 +2538,6 @@ def mk_config():
EXAMP_DEBUG_FLAG = '-g'
CPPFLAGS = '%s -DZ3DEBUG -D_DEBUG' % CPPFLAGS
else:
@@ -20,16 +11,16 @@ Index: scripts/mk_util.py
if GPROF:
CXXFLAGS += '-fomit-frame-pointer'
CPPFLAGS = '%s -DNDEBUG -D_EXTERNAL_RELEASE' % CPPFLAGS
-@@ -2836,7 +2835,7 @@ def mk_config():
- elif sysname == 'OpenBSD':
- CXXFLAGS = '%s -D_OPENBSD_' % CXXFLAGS
- OS_DEFINES = '-D_OPENBSD_'
+@@ -2551,7 +2550,7 @@ def mk_config():
+ elif sysname == 'Linux':
+ CXXFLAGS = '%s -D_LINUX_' % CXXFLAGS
+ OS_DEFINES = '-D_LINUX_'
-SO_EXT = '.so'
+SO_EXT = '.so.${LIBz3_VERSION}'
SLIBFLAGS = '-shared'
- elif sysname.startswith('CYGWIN'):
- CXXFLAGS = '%s -D_CYGWIN' % CXXFLAGS
-@@ -2852,9 +2851,9 @@ def mk_config():
+ SLIBEXTRAFLAGS = '%s -Wl,-soname,libz3.so' % SLIBEXTRAFLAGS
+ elif sysname == 'FreeBSD':
+@@ -2583,9 +2582,9 @@ def mk_config():
LIB_EXT= '.lib'
else:
raise MKException('Unsupported platform: %s' % sysname)
Index: pkg/PLIST
===
RCS file: /cvs/ports/math/z3/pkg/PLIST,v
retrieving revision 1.5
diff -u -p -r1.5 PLIST
--- pkg/PLIST 3 Mar 2019 09:16:17 - 1.5
+++ pkg/PLIST 16 Oct 2019 02:55:38 -
@@ -17,6 +17,7 @@ include/z3_version.h
lib/cmake/
lib/cmake/z3/
lib/cmake/z3/Z3Config.cmake
+lib/cmake/z3/Z3ConfigVersion.cmake
lib/cmake/z3/Z3Targets${MODCMAKE_BUILD_SUFFIX}
lib/cmake/z3/Z3Targets.cmake
@lib lib/libz3.so.${LIBz3_VERSION}
UPDATE: math/z3 to disable OpenMP
This simple patch switches OpenMP off.
Question though: as given, Makefile does not require some python
packages (py-setuptools, py-pip) to run z3 under python.
Should that be fixed?
Index: Makefile
===
RCS file: /cvs/ports/math/z3/Makefile,v
retrieving revision 1.13
diff -u -p -r1.13 Makefile
--- Makefile28 Apr 2019 20:51:42 - 1.13
+++ Makefile13 Jun 2019 21:12:23 -
@@ -4,7 +4,7 @@ COMMENT = Z3 theorem prover
VERSION = 4.8.4
DISTNAME = z3-${VERSION}
-REVISION = 1
+REVISION = 2
GH_ACCOUNT = Z3Prover
GH_PROJECT = z3
@@ -30,6 +30,7 @@ CONFIGURE_ARGS += -DENABLE_EXAMPLE_TARGE
-DINCLUDE_GIT_HASH=OFF \
-DINCLUDE_GIT_DESCRIBE=OFF \
-DBUILD_PYTHON_BINDINGS=ON \
+ -DUSE_OPENMP=OFF \
-DUSE_LIB_GMP=OFF
WRKDIST = ${WRKDIR}/z3-${DISTNAME}
Re: [UPDATE] math/z3
On 2019/06/05 16:10, Remi Pointel wrote:
> > The GH_* stuff in this is broken. If GH_ACCOUNT and GH_PROJECT are
> > present there should always be GH_TAGNAME or GH_COMMIT.
>
> Exactly, attached is the diff using GH_TAGNAME.
>
> I need to set DISTNAME because by default "DISTNAME =
> ${GH_PROJECT}-${GH_TAGNAME:C/^v//}" and PKGNAME because the upper Z of the
> tag of this release.
>
> Ok?
>
> Cheers,
>
> Remi.
> Index: Makefile
> ===
> RCS file: /cvs/ports/math/z3/Makefile,v
> retrieving revision 1.14
> diff -u -p -u -p -r1.14 Makefile
> --- Makefile 5 Jun 2019 05:44:54 - 1.14
> +++ Makefile 5 Jun 2019 13:58:28 -
> @@ -3,11 +3,13 @@
> COMMENT =Z3 theorem prover
>
> VERSION =4.8.5
> -DISTNAME = Z3-${VERSION}
> -PKGNAME =${DISTNAME:L}
>
> GH_ACCOUNT = Z3Prover
> GH_PROJECT = z3
> +GH_TAGNAME = ${GH_PROJECT:U}-${VERSION}
> +
> +DISTNAME = ${GH_TAGNAME}
> +PKGNAME =${DISTNAME:L}
>
> SHARED_LIBS =z3 2.0 # 4.8
>
Thanks, OK.
Re: [UPDATE] math/z3
The GH_* stuff in this is broken. If GH_ACCOUNT and GH_PROJECT are
present there should always be GH_TAGNAME or GH_COMMIT.
Exactly, attached is the diff using GH_TAGNAME.
I need to set DISTNAME because by default "DISTNAME =
${GH_PROJECT}-${GH_TAGNAME:C/^v//}" and PKGNAME because the upper Z of
the tag of this release.
Ok?
Cheers,
Remi.
Index: Makefile
===
RCS file: /cvs/ports/math/z3/Makefile,v
retrieving revision 1.14
diff -u -p -u -p -r1.14 Makefile
--- Makefile 5 Jun 2019 05:44:54 - 1.14
+++ Makefile 5 Jun 2019 13:58:28 -
@@ -3,11 +3,13 @@
COMMENT = Z3 theorem prover
VERSION = 4.8.5
-DISTNAME = Z3-${VERSION}
-PKGNAME = ${DISTNAME:L}
GH_ACCOUNT = Z3Prover
GH_PROJECT = z3
+GH_TAGNAME = ${GH_PROJECT:U}-${VERSION}
+
+DISTNAME = ${GH_TAGNAME}
+PKGNAME = ${DISTNAME:L}
SHARED_LIBS = z3 2.0 # 4.8
Re: [UPDATE] math/z3
On 2019/06/04 14:45, Remi Pointel wrote:
> Hi,
>
> this diff updates z3 to latest release.
>
> Ok?
>
> Cheers,
>
> Remi.
> Index: Makefile
> ===
> RCS file: /cvs/ports/math/z3/Makefile,v
> retrieving revision 1.13
> diff -u -p -u -p -r1.13 Makefile
> --- Makefile 28 Apr 2019 20:51:42 - 1.13
> +++ Makefile 4 Jun 2019 12:45:10 -
> @@ -2,14 +2,14 @@
>
> COMMENT =Z3 theorem prover
>
> -VERSION =4.8.4
> -DISTNAME = z3-${VERSION}
> -REVISION = 1
> +VERSION =4.8.5
> +DISTNAME = Z3-${VERSION}
> +PKGNAME =${DISTNAME:L}
>
> GH_ACCOUNT = Z3Prover
> GH_PROJECT = z3
The GH_* stuff in this is broken. If GH_ACCOUNT and GH_PROJECT are
present there should always be GH_TAGNAME or GH_COMMIT.
Re: [UPDATE] math/z3
On Tue, Jun 04, 2019 at 02:45:46PM +0200, Remi Pointel wrote: > this diff updates z3 to latest release. Brief summay of what changed or why you bumped the major? Or a link?
[UPDATE] math/z3
Hi,
this diff updates z3 to latest release.
Ok?
Cheers,
Remi.
Index: Makefile
===
RCS file: /cvs/ports/math/z3/Makefile,v
retrieving revision 1.13
diff -u -p -u -p -r1.13 Makefile
--- Makefile 28 Apr 2019 20:51:42 - 1.13
+++ Makefile 4 Jun 2019 12:45:10 -
@@ -2,14 +2,14 @@
COMMENT = Z3 theorem prover
-VERSION = 4.8.4
-DISTNAME = z3-${VERSION}
-REVISION = 1
+VERSION = 4.8.5
+DISTNAME = Z3-${VERSION}
+PKGNAME = ${DISTNAME:L}
GH_ACCOUNT = Z3Prover
GH_PROJECT = z3
-SHARED_LIBS = z3 1.0
+SHARED_LIBS = z3 2.0 # 4.8
CATEGORIES = math
Index: distinfo
===
RCS file: /cvs/ports/math/z3/distinfo,v
retrieving revision 1.5
diff -u -p -u -p -r1.5 distinfo
--- distinfo 3 Mar 2019 09:16:17 - 1.5
+++ distinfo 4 Jun 2019 12:45:10 -
@@ -1,2 +1,2 @@
-SHA256 (z3-4.8.4.tar.gz) = Whj+YWwqMLVuWy9bnwP0Bc3yQ1cRUX/3CwdqATlu9gE=
-SIZE (z3-4.8.4.tar.gz) = 4117081
+SHA256 (Z3-4.8.5.tar.gz) = To4jKIfd+mQ622ow3NN0PLL6ZZFzX70wK0n3AozcA2M=
+SIZE (Z3-4.8.5.tar.gz) = 4177051
Re: [UPDATE] math/z3
On Sat Jan 19, 2019 at 10:56:35AM +0100, Remi Pointel wrote:
> Hi,
>
> this is the diff to update z3 to latest release.
>
> Ok?
>
> Cheers,
>
> Remi.
Maybe it's a good idea to move to cmake as build system? Perhaps
consumers more happy with the cmake targets!?
RS
Index: Makefile
===
RCS file: /cvs/ports/math/z3/Makefile,v
retrieving revision 1.10
diff -u -p -u -p -r1.10 Makefile
--- Makefile15 Dec 2018 12:43:40 - 1.10
+++ Makefile19 Jan 2019 11:55:21 -
@@ -2,7 +2,7 @@
COMMENT = Z3 theorem prover
-VERSION = 4.8.3
+VERSION = 4.8.4
DISTNAME = z3-${VERSION}
GH_ACCOUNT = Z3Prover
@@ -17,19 +17,19 @@ WANTLIB += c m pthread ${COMPILER_LIBCXX
# MIT
PERMIT_PACKAGE_CDROM = Yes
-CONFIGURE_STYLE = simple
-
-CONFIGURE_ARGS += --prefix=${PREFIX} \
- --python
-
# c++11
COMPILER = base-clang ports-gcc
-MODULES = lang/python
+MODULES = devel/cmake \
+ lang/python
+
+CONFIGURE_ARGS += -DENABLE_EXAMPLE_TARGETS=ON \
+ -DINCLUDE_GIT_HASH=OFF \
+ -DINCLUDE_GIT_DESCRIBE=OFF \
+ -DBUILD_PYTHON_BINDINGS=ON \
+ -DUSE_LIB_GMP=OFF
WRKDIST = ${WRKDIR}/z3-${DISTNAME}
-WRKCONF = ${WRKSRC}
-WRKBUILD = ${WRKSRC}/build
pre-configure:
${SUBST_CMD} ${WRKSRC}/scripts/mk_util.py
Index: distinfo
===
RCS file: /cvs/ports/math/z3/distinfo,v
retrieving revision 1.4
diff -u -p -u -p -r1.4 distinfo
--- distinfo15 Dec 2018 12:43:40 - 1.4
+++ distinfo19 Jan 2019 11:55:21 -
@@ -1,2 +1,2 @@
-SHA256 (z3-4.8.3.tar.gz) = IWILaMNzzeoNOyzyQCC+Ts+yLt3GYpZj9unOMc/ceN4=
-SIZE (z3-4.8.3.tar.gz) = 4119116
+SHA256 (z3-4.8.4.tar.gz) = Whj+YWwqMLVuWy9bnwP0Bc3yQ1cRUX/3CwdqATlu9gE=
+SIZE (z3-4.8.4.tar.gz) = 4117081
Index: patches/patch-cmake_cxx_compiler_flags_overrides_cmake
===
RCS file: patches/patch-cmake_cxx_compiler_flags_overrides_cmake
diff -N patches/patch-cmake_cxx_compiler_flags_overrides_cmake
--- /dev/null 1 Jan 1970 00:00:00 -
+++ patches/patch-cmake_cxx_compiler_flags_overrides_cmake 19 Jan 2019
11:55:21 -
@@ -0,0 +1,13 @@
+$OpenBSD$
+
+Index: cmake/cxx_compiler_flags_overrides.cmake
+--- cmake/cxx_compiler_flags_overrides.cmake.orig
cmake/cxx_compiler_flags_overrides.cmake
+@@ -9,6 +9,6 @@ if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang") OR ("
+ set(CMAKE_CXX_FLAGS_INIT "")
+ set(CMAKE_CXX_FLAGS_DEBUG_INIT "-g -O0")
+ set(CMAKE_CXX_FLAGS_MINSIZEREL_INIT "-Os -DNDEBUG")
+- set(CMAKE_CXX_FLAGS_RELEASE_INIT "-O3 -DNDEBUG")
++ set(CMAKE_CXX_FLAGS_RELEASE_INIT "-DNDEBUG")
+ set(CMAKE_CXX_FLAGS_RELWITHDEBINFO_INIT "-O2 -g -DNDEBUG")
+ endif()
Index: patches/patch-scripts_mk_util_py
===
RCS file: /cvs/ports/math/z3/patches/patch-scripts_mk_util_py,v
retrieving revision 1.2
diff -u -p -u -p -r1.2 patch-scripts_mk_util_py
--- patches/patch-scripts_mk_util_py24 Nov 2018 00:57:15 - 1.2
+++ patches/patch-scripts_mk_util_py19 Jan 2019 11:55:21 -
@@ -3,7 +3,7 @@ $OpenBSD: patch-scripts_mk_util_py,v 1.2
Index: scripts/mk_util.py
--- scripts/mk_util.py.orig
+++ scripts/mk_util.py
-@@ -49,7 +49,7 @@ C_COMPILERS=['gcc', 'clang']
+@@ -50,7 +50,7 @@ C_COMPILERS=['gcc', 'clang']
CSC_COMPILERS=['csc', 'mcs']
JAVAC=None
JAR=None
@@ -12,7 +12,7 @@ Index: scripts/mk_util.py
BUILD_DIR='build'
REV_BUILD_DIR='..'
SRC_DIR='src'
-@@ -2494,7 +2494,6 @@ def mk_config():
+@@ -2801,7 +2801,6 @@ def mk_config():
EXAMP_DEBUG_FLAG = '-g'
CPPFLAGS = '%s -DZ3DEBUG -D_DEBUG' % CPPFLAGS
else:
@@ -20,7 +20,7 @@ Index: scripts/mk_util.py
if GPROF:
CXXFLAGS += '-fomit-frame-pointer'
CPPFLAGS = '%s -DNDEBUG -D_EXTERNAL_RELEASE' % CPPFLAGS
-@@ -2528,7 +2527,7 @@ def mk_config():
+@@ -2836,7 +2835,7 @@ def mk_config():
elif sysname == 'OpenBSD':
CXXFLAGS = '%s -D_OPENBSD_' % CXXFLAGS
OS_DEFINES = '-D_OPENBSD_'
@@ -29,7 +29,7 @@ Index: scripts/mk_util.py
SLIBFLAGS = '-shared'
elif sysname.startswith('CYGWIN'):
CXXFLAGS = '%s -D_CYGWIN' % CXXFLAGS
-@@ -2544,9 +2543,9 @@ def mk_config():
+@@ -2852,9 +2851,9 @@ def mk_config():
LIB_EXT= '.lib'
else:
raise MKException('Unsupported platform: %s' % sysname)
@@ -38,6 +38,6 @@ Index: scripts/mk_util.py
if is64():
-if not sysname.startswith('CYGWIN') and not
sysname.startswith('MSYS') and not sysname.startswith('MINGW'):
-CXXFLAGS = '%s -fPIC' % CXXFLAGS
- CPPFLAGS = '%s -D_AMD64_' %
[UPDATE] math/z3
Hi,
this is the diff to update z3 to latest release.
Ok?
Cheers,
Remi.
Index: Makefile
===
RCS file: /cvs/ports/math/z3/Makefile,v
retrieving revision 1.10
diff -u -p -u -p -r1.10 Makefile
--- Makefile 15 Dec 2018 12:43:40 - 1.10
+++ Makefile 19 Jan 2019 09:55:04 -
@@ -2,7 +2,7 @@
COMMENT = Z3 theorem prover
-VERSION = 4.8.3
+VERSION = 4.8.4
DISTNAME = z3-${VERSION}
GH_ACCOUNT = Z3Prover
Index: distinfo
===
RCS file: /cvs/ports/math/z3/distinfo,v
retrieving revision 1.4
diff -u -p -u -p -r1.4 distinfo
--- distinfo 15 Dec 2018 12:43:40 - 1.4
+++ distinfo 19 Jan 2019 09:55:04 -
@@ -1,2 +1,2 @@
-SHA256 (z3-4.8.3.tar.gz) = IWILaMNzzeoNOyzyQCC+Ts+yLt3GYpZj9unOMc/ceN4=
-SIZE (z3-4.8.3.tar.gz) = 4119116
+SHA256 (z3-4.8.4.tar.gz) = Whj+YWwqMLVuWy9bnwP0Bc3yQ1cRUX/3CwdqATlu9gE=
+SIZE (z3-4.8.4.tar.gz) = 4117081
Index: patches/patch-scripts_mk_util_py
===
RCS file: /cvs/ports/math/z3/patches/patch-scripts_mk_util_py,v
retrieving revision 1.2
diff -u -p -u -p -r1.2 patch-scripts_mk_util_py
--- patches/patch-scripts_mk_util_py 24 Nov 2018 00:57:15 - 1.2
+++ patches/patch-scripts_mk_util_py 19 Jan 2019 09:55:04 -
@@ -3,7 +3,7 @@ $OpenBSD: patch-scripts_mk_util_py,v 1.2
Index: scripts/mk_util.py
--- scripts/mk_util.py.orig
+++ scripts/mk_util.py
-@@ -49,7 +49,7 @@ C_COMPILERS=['gcc', 'clang']
+@@ -50,7 +50,7 @@ C_COMPILERS=['gcc', 'clang']
CSC_COMPILERS=['csc', 'mcs']
JAVAC=None
JAR=None
@@ -12,7 +12,7 @@ Index: scripts/mk_util.py
BUILD_DIR='build'
REV_BUILD_DIR='..'
SRC_DIR='src'
-@@ -2494,7 +2494,6 @@ def mk_config():
+@@ -2801,7 +2801,6 @@ def mk_config():
EXAMP_DEBUG_FLAG = '-g'
CPPFLAGS = '%s -DZ3DEBUG -D_DEBUG' % CPPFLAGS
else:
@@ -20,7 +20,7 @@ Index: scripts/mk_util.py
if GPROF:
CXXFLAGS += '-fomit-frame-pointer'
CPPFLAGS = '%s -DNDEBUG -D_EXTERNAL_RELEASE' % CPPFLAGS
-@@ -2528,7 +2527,7 @@ def mk_config():
+@@ -2836,7 +2835,7 @@ def mk_config():
elif sysname == 'OpenBSD':
CXXFLAGS = '%s -D_OPENBSD_' % CXXFLAGS
OS_DEFINES = '-D_OPENBSD_'
@@ -29,7 +29,7 @@ Index: scripts/mk_util.py
SLIBFLAGS = '-shared'
elif sysname.startswith('CYGWIN'):
CXXFLAGS = '%s -D_CYGWIN' % CXXFLAGS
-@@ -2544,9 +2543,9 @@ def mk_config():
+@@ -2852,9 +2851,9 @@ def mk_config():
LIB_EXT= '.lib'
else:
raise MKException('Unsupported platform: %s' % sysname)
@@ -38,6 +38,6 @@ Index: scripts/mk_util.py
if is64():
-if not sysname.startswith('CYGWIN') and not sysname.startswith('MSYS') and not sysname.startswith('MINGW'):
-CXXFLAGS = '%s -fPIC' % CXXFLAGS
- CPPFLAGS = '%s -D_AMD64_' % CPPFLAGS
if sysname == 'Linux':
CPPFLAGS = '%s -D_USE_THREAD_LOCAL' % CPPFLAGS
+ elif not LINUX_X64:
Re: [UPDATE] math/z3
OK În 14 decembrie 2018 15:02:35 EET, Remi Pointel a scris: >Hi, > >this diff updates z3 to latest release. > >Ok? > >Cheers, > >Remi.
[UPDATE] math/z3
Hi,
this diff updates z3 to latest release.
Ok?
Cheers,
Remi.
Index: Makefile
===
RCS file: /cvs/ports/math/z3/Makefile,v
retrieving revision 1.9
diff -u -p -u -p -r1.9 Makefile
--- Makefile 24 Nov 2018 00:57:15 - 1.9
+++ Makefile 14 Dec 2018 13:01:40 -
@@ -2,14 +2,13 @@
COMMENT = Z3 theorem prover
-VERSION = 4.7.1
+VERSION = 4.8.3
DISTNAME = z3-${VERSION}
-REVISION = 1
GH_ACCOUNT = Z3Prover
GH_PROJECT = z3
-SHARED_LIBS = z3 0.0
+SHARED_LIBS = z3 1.0
CATEGORIES = math
Index: distinfo
===
RCS file: /cvs/ports/math/z3/distinfo,v
retrieving revision 1.3
diff -u -p -u -p -r1.3 distinfo
--- distinfo 18 Jun 2018 08:15:11 - 1.3
+++ distinfo 14 Dec 2018 13:01:40 -
@@ -1,2 +1,2 @@
-SHA256 (z3-4.7.1.tar.gz) = o1Pj2gDNr/0lgFLMFAbvyFRgaFUiKrS/1WecWK9cEcc=
-SIZE (z3-4.7.1.tar.gz) = 4015416
+SHA256 (z3-4.8.3.tar.gz) = IWILaMNzzeoNOyzyQCC+Ts+yLt3GYpZj9unOMc/ceN4=
+SIZE (z3-4.8.3.tar.gz) = 4119116
Index: pkg/PLIST
===
RCS file: /cvs/ports/math/z3/pkg/PLIST,v
retrieving revision 1.3
diff -u -p -u -p -r1.3 PLIST
--- pkg/PLIST 15 Sep 2018 13:27:29 - 1.3
+++ pkg/PLIST 14 Dec 2018 13:01:40 -
@@ -7,13 +7,13 @@ include/z3_api.h
include/z3_ast_containers.h
include/z3_fixedpoint.h
include/z3_fpa.h
-include/z3_interp.h
include/z3_macros.h
include/z3_optimization.h
include/z3_polynomial.h
include/z3_rcf.h
include/z3_spacer.h
include/z3_v1.h
+include/z3_version.h
@lib lib/libz3.so.${LIBz3_VERSION}
lib/python${MODPY_VERSION}/site-packages/z3/
lib/python${MODPY_VERSION}/site-packages/z3/__init__.py
[UPDATE] math/z3
Hi,
attached is a diff to update z3 to latest release.
Ok?
Cheers,
Remi.
Index: Makefile
===
RCS file: /cvs/ports/math/z3/Makefile,v
retrieving revision 1.5
diff -u -p -u -p -r1.5 Makefile
--- Makefile 10 Apr 2018 08:17:38 - 1.5
+++ Makefile 18 Jun 2018 05:49:07 -
@@ -2,7 +2,7 @@
COMMENT = z3 theorem prover
-VERSION = 4.6.0
+VERSION = 4.7.1
DISTNAME = z3-${VERSION}
GH_ACCOUNT = Z3Prover
Index: distinfo
===
RCS file: /cvs/ports/math/z3/distinfo,v
retrieving revision 1.2
diff -u -p -u -p -r1.2 distinfo
--- distinfo 10 Apr 2018 08:17:38 - 1.2
+++ distinfo 18 Jun 2018 05:49:07 -
@@ -1,2 +1,2 @@
-SHA256 (z3-4.6.0.tar.gz) = UR2jHR+YXPDHmy3gW9pOBXNxulGXadFUb/ceEwT+U8k=
-SIZE (z3-4.6.0.tar.gz) = 3987830
+SHA256 (z3-4.7.1.tar.gz) = o1Pj2gDNr/0lgFLMFAbvyFRgaFUiKrS/1WecWK9cEcc=
+SIZE (z3-4.7.1.tar.gz) = 4015416
Re: update: math/z3
Le 10-04-2018 06:26, Matthew Martin a écrit : Update z3; builds here with clang 6. Enable tests while here. - Matthew Martin Hi, thanks it's commited. Cheers, Remi.
update: math/z3
Update z3; builds here with clang 6. Enable tests while here.
- Matthew Martin
diff --git Makefile Makefile
index 6fe70abc40a..b32659d5940 100644
--- Makefile
+++ Makefile
@@ -2,9 +2,8 @@
COMMENT = z3 theorem prover
-VERSION = 4.5.0
+VERSION = 4.6.0
DISTNAME = z3-${VERSION}
-REVISION = 0
GH_ACCOUNT = Z3Prover
GH_PROJECT = z3
@@ -25,11 +24,12 @@ MODULES = lang/python
WRKDIST = ${WRKDIR}/z3-${DISTNAME}
-NO_TEST = Yes
-
do-build:
cd ${WRKSRC}/build && make
+do-test:
+ cd ${WRKSRC}/build && make test
+
do-install:
cd ${WRKSRC}/build && make install DESTDIR=""
diff --git distinfo distinfo
index 367c197e8d9..78a13056b2b 100644
--- distinfo
+++ distinfo
@@ -1,2 +1,2 @@
-SHA256 (z3-4.5.0.tar.gz) = rq4dI5xeBqwYO+fdhTd1uEaY2xJlyyJY5ZGKKDctSgw=
-SIZE (z3-4.5.0.tar.gz) = 3573695
+SHA256 (z3-4.6.0.tar.gz) = UR2jHR+YXPDHmy3gW9pOBXNxulGXadFUb/ceEwT+U8k=
+SIZE (z3-4.6.0.tar.gz) = 3987830
diff --git pkg/PLIST pkg/PLIST
index 0d452ebdc7f..ad83b890997 100644
--- pkg/PLIST
+++ pkg/PLIST
@@ -12,6 +12,7 @@ include/z3_macros.h
include/z3_optimization.h
include/z3_polynomial.h
include/z3_rcf.h
+include/z3_spacer.h
include/z3_v1.h
lib/libz3.so
lib/python${MODPY_VERSION}/site-packages/z3/
