Frederic Cambus <f...@statdns.com> 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 -0000 1.25
> +++ Makefile 3 May 2022 15:16:12 -0000
> @@ -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 -0000 1.9
> +++ distinfo 3 May 2022 15:16:12 -0000
> @@ -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 -0000 1.7
> +++ patches/patch-scripts_mk_util_py 3 May 2022 15:16:12 -0000
> @@ -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)
