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)
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}
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?
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_'
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.
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.
