pkgsrc-Changes-HG archive
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index][Old Index]
[pkgsrc/trunk]: pkgsrc/math/z3 Update math/z3 to version 4.5.0
details: https://anonhg.NetBSD.org/pkgsrc/rev/5500dc982275
branches: trunk
changeset: 377043:5500dc982275
user: khorben <khorben%pkgsrc.org@localhost>
date: Tue Mar 13 00:31:16 2018 +0000
description:
Update math/z3 to version 4.5.0
>From the release notes:
New features:
- New theories of strings and sequences.
- Incremental consequence finder for finite domains.
- CMake build system (thanks @delcypher).
- Updated and improved OCaml API (thanks @martin-neuhaeusser).
- Updated and improved Java API (thanks @cheshire).
- New resource limit facilities to avoid non-deterministic timeout behaviour.
- New bit-vector simplification and ackermannization tactics (thanks @MikolasJanota, @nunoplopes).
- QSAT: a new solver for quantified arithmetic problems. See:
Bjorner, Janota: Playing with Quantified Satisfaction, LPAR 2016.
A multitude of bugs has been fixed.
I am about to commit a separate package for the Python bindings.
Coordinated with dholland@
diffstat:
math/z3/Makefile | 29 +---
math/z3/Makefile.common | 26 +++
math/z3/PLIST | 42 ++--
math/z3/buildlink3.mk | 13 +
math/z3/distinfo | 20 +-
math/z3/options.mk | 4 +-
math/z3/patches/patch-configure | 12 +
math/z3/patches/patch-scripts_mk__util.py | 227 ++++++++++++++++++++++++++--
math/z3/patches/patch-src_util_debug.cpp | 15 -
math/z3/patches/patch-src_util_mpz.cpp | 15 -
math/z3/patches/patch-src_util_stopwatch.h | 16 ++
11 files changed, 305 insertions(+), 114 deletions(-)
diffs (truncated from 501 to 300 lines):
diff -r ed0c44f10369 -r 5500dc982275 math/z3/Makefile
--- a/math/z3/Makefile Mon Mar 12 20:51:30 2018 +0000
+++ b/math/z3/Makefile Tue Mar 13 00:31:16 2018 +0000
@@ -1,32 +1,9 @@
-# $NetBSD: Makefile,v 1.7 2018/02/27 08:34:16 wiz Exp $
-
-DISTNAME= z3-4.4.1
-GITHUB_TAG= ${DISTNAME}
-PKGREVISION= 5
-CATEGORIES= math
-MASTER_SITES= ${MASTER_SITE_GITHUB:=Z3Prover/}
-PATCHFILES+= z3-jumbo-patch-20151123.gz
-SITES.z3-jumbo-patch-20151123.gz=\
- http://www.NetBSD.org/~dholland/patchkits/z3/
-PATCH_DIST_STRIP= -p1
+# $NetBSD: Makefile,v 1.8 2018/03/13 00:31:16 khorben Exp $
-MAINTAINER= dholland%NetBSD.org@localhost
-HOMEPAGE= https://github.com/Z3Prover/z3/
-COMMENT= The Z3 theorem prover / SMT solver
-LICENSE= mit
+.include "Makefile.common"
-WRKSRC= ${WRKDIR}/z3-${DISTNAME}
-HAS_CONFIGURE= yes
-USE_LANGUAGES= c c++
-BUILD_DIRS= build
-PY_PATCHPLIST= yes
-
-PYTHON_VERSIONS_ACCEPTED= 27
-
-CONFIGURE_ENV+= PYTHON=${PYTHONBIN}
-CONFIGURE_ARGS+= --destdir=${DESTDIR} --prefix=${PREFIX}
+COMMENT= The Z3 theorem prover / SMT solver
.include "options.mk"
-.include "../../lang/python/extension.mk"
.include "../../mk/bsd.pkg.mk"
diff -r ed0c44f10369 -r 5500dc982275 math/z3/Makefile.common
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/math/z3/Makefile.common Tue Mar 13 00:31:16 2018 +0000
@@ -0,0 +1,26 @@
+# $NetBSD: Makefile.common,v 1.1 2018/03/13 00:31:16 khorben Exp $
+#
+# used by wip/py-z3/Makefile
+# used by wip/z3/Makefile
+
+DISTNAME= z3-4.5.0
+GITHUB_TAG= ${DISTNAME}
+CATEGORIES= math
+MASTER_SITES= ${MASTER_SITE_GITHUB:=Z3Prover/}
+DISTINFO_FILE= ${.CURDIR}/../../wip/z3/distinfo
+PATCHDIR?= ${.CURDIR}/../../wip/z3/patches
+
+MAINTAINER= dholland%NetBSD.org@localhost
+HOMEPAGE= https://github.com/Z3Prover/z3/
+LICENSE= mit
+
+WRKSRC= ${WRKDIR}/z3-${DISTNAME}
+HAS_CONFIGURE= yes
+USE_LANGUAGES= c c++
+BUILD_DIRS= build
+
+CONFIGURE_ENV+= PYTHON=${PYTHONBIN}
+CONFIGURE_ARGS+= --destdir=${DESTDIR}
+CONFIGURE_ARGS+= --prefix=${PREFIX}
+
+.include "../../lang/python/tool.mk"
diff -r ed0c44f10369 -r 5500dc982275 math/z3/PLIST
--- a/math/z3/PLIST Mon Mar 12 20:51:30 2018 +0000
+++ b/math/z3/PLIST Tue Mar 13 00:31:16 2018 +0000
@@ -1,34 +1,32 @@
-@comment $NetBSD: PLIST,v 1.1 2015/11/24 05:45:58 dholland Exp $
+@comment $NetBSD: PLIST,v 1.2 2018/03/13 00:31:16 khorben Exp $
bin/z3
include/z3++.h
include/z3.h
include/z3_algebraic.h
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_v1.h
lib/libz3.so
-${PYSITELIB}/libz3.so
-${PYSITELIB}/z3.py
-${PYSITELIB}/z3.pyc
-${PYSITELIB}/z3consts.py
-${PYSITELIB}/z3consts.pyc
-${PYSITELIB}/z3core.py
-${PYSITELIB}/z3core.pyc
-${PYSITELIB}/z3num.py
-${PYSITELIB}/z3num.pyc
-${PYSITELIB}/z3poly.py
-${PYSITELIB}/z3poly.pyc
-${PYSITELIB}/z3printer.py
-${PYSITELIB}/z3printer.pyc
-${PYSITELIB}/z3rcf.py
-${PYSITELIB}/z3rcf.pyc
-${PYSITELIB}/z3test.py
-${PYSITELIB}/z3test.pyc
-${PYSITELIB}/z3types.py
-${PYSITELIB}/z3types.pyc
-${PYSITELIB}/z3util.py
-${PYSITELIB}/z3util.pyc
+${PLIST.ocaml}lib/ocaml/site-lib/Z3/META
+${PLIST.ocaml}lib/ocaml/site-lib/Z3/dllz3ml.so
+${PLIST.ocaml}lib/ocaml/site-lib/Z3/libz3ml.a
+${PLIST.ocaml}lib/ocaml/site-lib/Z3/z3.cmi
+${PLIST.ocaml}lib/ocaml/site-lib/Z3/z3.cmx
+${PLIST.ocaml}lib/ocaml/site-lib/Z3/z3.mli
+${PLIST.ocaml}lib/ocaml/site-lib/Z3/z3enums.cmi
+${PLIST.ocaml}lib/ocaml/site-lib/Z3/z3enums.cmx
+${PLIST.ocaml}lib/ocaml/site-lib/Z3/z3enums.mli
+${PLIST.ocaml}lib/ocaml/site-lib/Z3/z3ml.a
+${PLIST.ocaml}lib/ocaml/site-lib/Z3/z3ml.cma
+${PLIST.ocaml}lib/ocaml/site-lib/Z3/z3ml.cmxa
+${PLIST.ocaml}lib/ocaml/site-lib/Z3/z3ml.cmxs
+${PLIST.ocaml}lib/ocaml/site-lib/Z3/z3native.cmi
+${PLIST.ocaml}lib/ocaml/site-lib/Z3/z3native.cmx
+${PLIST.ocaml}lib/ocaml/site-lib/Z3/z3native.mli
diff -r ed0c44f10369 -r 5500dc982275 math/z3/buildlink3.mk
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/math/z3/buildlink3.mk Tue Mar 13 00:31:16 2018 +0000
@@ -0,0 +1,13 @@
+# $NetBSD: buildlink3.mk,v 1.1 2018/03/13 00:31:16 khorben Exp $
+
+BUILDLINK_TREE+= z3
+
+.if !defined(Z3_BUILDLINK3_MK)
+Z3_BUILDLINK3_MK:=
+
+BUILDLINK_API_DEPENDS.z3+= z3>=4.5.0
+BUILDLINK_PKGSRCDIR.z3?= ../../wip/z3
+
+.endif # Z3_BUILDLINK3_MK
+
+BUILDLINK_TREE+= -z3
diff -r ed0c44f10369 -r 5500dc982275 math/z3/distinfo
--- a/math/z3/distinfo Mon Mar 12 20:51:30 2018 +0000
+++ b/math/z3/distinfo Tue Mar 13 00:31:16 2018 +0000
@@ -1,13 +1,9 @@
-$NetBSD: distinfo,v 1.3 2018/02/23 17:04:43 khorben Exp $
+$NetBSD: distinfo,v 1.4 2018/03/13 00:31:16 khorben Exp $
-SHA1 (z3-4.4.1.tar.gz) = 60094acaa53459ec694899aca9f17aa830875610
-RMD160 (z3-4.4.1.tar.gz) = 2c891e115a5d097dbbda53c1b322c65bc5b679f7
-SHA512 (z3-4.4.1.tar.gz) = 76991a24f47f2b53ceb8d7a9a6be19913c57994ffb6cf6acfe30f61b2e73959cf02a99f656053594fccb5aaf4d1f44b3ae7e51f1c8953b213d738ceeeaea74f8
-Size (z3-4.4.1.tar.gz) = 3347371 bytes
-SHA1 (z3-jumbo-patch-20151123.gz) = d31b8840575536104680bb624b15cc1c2084a7fb
-RMD160 (z3-jumbo-patch-20151123.gz) = eb74bd41125e1b07a7f873774a2c354e3c8ca378
-SHA512 (z3-jumbo-patch-20151123.gz) = c23d363bf53b40c3ccbfc10d03ef3621d6abfa9cf86375e7e853e85a0971db70992173df04df1a895e16d4a9b533e955953455a7533889963d2920a4b48d0056
-Size (z3-jumbo-patch-20151123.gz) = 4395 bytes
-SHA1 (patch-scripts_mk__util.py) = 84ccd3fa33a3fcffa53af6f838f6caacdfec40a8
-SHA1 (patch-src_util_debug.cpp) = 607ea4e078884920a3034cf00779dce25fc8e623
-SHA1 (patch-src_util_mpz.cpp) = 69988bec1472df14209ae0dbfdc8a94c9e71cc82
+SHA1 (z3-4.5.0.tar.gz) = 6f4e94e025fcc2fa2896524d8fbb9de0b3033854
+RMD160 (z3-4.5.0.tar.gz) = 81121307ac83f42989da49efda31964a94f7f5d5
+SHA512 (z3-4.5.0.tar.gz) = 1ebc2c908d90b6b879f1e819c864ff894613276af47a440f27cf94968c195656952434754c3eb20f4bdbdd8497d227d22e1b4821c0d320b11052b5648d9e2dc7
+Size (z3-4.5.0.tar.gz) = 3573695 bytes
+SHA1 (patch-configure) = 8d5fe787f15fe781c3c23cee27058f898de8c95e
+SHA1 (patch-scripts_mk__util.py) = f0a7cfabdbf9b6c1eb92e75f381d8a3f8a088d35
+SHA1 (patch-src_util_stopwatch.h) = dbeab175ed4f507d5378f1966f8ed173c4c9a9a7
diff -r ed0c44f10369 -r 5500dc982275 math/z3/options.mk
--- a/math/z3/options.mk Mon Mar 12 20:51:30 2018 +0000
+++ b/math/z3/options.mk Tue Mar 13 00:31:16 2018 +0000
@@ -1,4 +1,4 @@
-# $NetBSD: options.mk,v 1.2 2018/03/11 06:14:45 dholland Exp $
+# $NetBSD: options.mk,v 1.3 2018/03/13 00:31:16 khorben Exp $
PKG_OPTIONS_VAR= PKG_OPTIONS.z3
PKG_SUPPORTED_OPTIONS= ocaml java
@@ -6,10 +6,12 @@
.include "../../mk/bsd.options.mk"
+PLIST_VARS+= ocaml
.if !empty(PKG_OPTIONS:Mocaml)
CONFIGURE_ARGS+= --ml
.include "../../math/ocaml-num/buildlink3.mk"
.include "../../lang/ocaml/buildlink3.mk"
+PLIST.ocaml= yes
.endif
.if !empty(PKG_OPTIONS:Mjava)
diff -r ed0c44f10369 -r 5500dc982275 math/z3/patches/patch-configure
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/math/z3/patches/patch-configure Tue Mar 13 00:31:16 2018 +0000
@@ -0,0 +1,12 @@
+$NetBSD: patch-configure,v 1.1 2018/03/13 00:31:16 khorben Exp $
+
+Fix parameter expansion when configuring Z3.
+
+--- configure.orig 2016-11-07 22:02:30.000000000 +0000
++++ configure
+@@ -14,4 +14,4 @@ if ! $PYTHON -c "print('testing')" > /de
+ exit 1
+ fi
+
+-$PYTHON scripts/mk_make.py $*
++$PYTHON scripts/mk_make.py "$@"
diff -r ed0c44f10369 -r 5500dc982275 math/z3/patches/patch-scripts_mk__util.py
--- a/math/z3/patches/patch-scripts_mk__util.py Mon Mar 12 20:51:30 2018 +0000
+++ b/math/z3/patches/patch-scripts_mk__util.py Tue Mar 13 00:31:16 2018 +0000
@@ -1,28 +1,209 @@
-$NetBSD: patch-scripts_mk__util.py,v 1.2 2018/02/23 17:04:43 khorben Exp $
-
-For pkgsrc, use site-packages rather than dist-packages.
-Add support for DESTDIR.
+$NetBSD: patch-scripts_mk__util.py,v 1.3 2018/03/13 00:31:16 khorben Exp $
-diff -r 59247c69b92d scripts/mk_util.py
---- scripts/mk_util.py.orig 2018-02-22 23:06:23.490379838 +0000
+--- scripts/mk_util.py.orig 2016-11-07 22:02:30.000000000 +0000
+++ scripts/mk_util.py
-@@ -637,7 +637,7 @@ def parse_options():
+@@ -69,6 +69,7 @@ IS_WINDOWS=False
+ IS_LINUX=False
+ IS_OSX=False
+ IS_FREEBSD=False
++IS_NETBSD=False
+ IS_OPENBSD=False
+ IS_CYGWIN=False
+ IS_CYGWIN_MINGW=False
+@@ -95,6 +96,7 @@ VER_MINOR=None
+ VER_BUILD=None
+ VER_REVISION=None
+ PREFIX=sys.prefix
++DESTDIR=""
+ GMP=False
+ FOCI2=False
+ FOCI2LIB=''
+@@ -139,6 +141,9 @@ def is_linux():
+ def is_freebsd():
+ return IS_FREEBSD
+
++def is_netbsd():
++ return IS_NETBSD
++
+ def is_openbsd():
+ return IS_OPENBSD
+
+@@ -607,6 +612,8 @@ elif os.name == 'posix':
+ IS_LINUX=True
+ elif os.uname()[0] == 'FreeBSD':
+ IS_FREEBSD=True
++ elif os.uname()[0] == 'NetBSD':
++ IS_NETBSD=True
+ elif os.uname()[0] == 'OpenBSD':
+ IS_OPENBSD=True
+ elif os.uname()[0][:6] == 'CYGWIN':
+@@ -623,6 +630,7 @@ def display_help(exit_code):
+ print(" -s, --silent do not print verbose messages.")
+ if not IS_WINDOWS:
+ print(" -p <dir>, --prefix=<dir> installation prefix (default: %s)." % PREFIX)
++ print(" -D <dir>, --destdir=<dir> installation chroot (default: none).")
+ else:
+ print(" --parallel=num use cl option /MP with 'num' parallel processes")
+ print(" --pypkgdir=<dir> Force a particular Python package directory (default %s)" % PYTHON_PACKAGE_DIR)
+@@ -677,13 +685,13 @@ def display_help(exit_code):
+ # Parse configuration option for mk_make script
+ def parse_options():
+ global VERBOSE, DEBUG_MODE, IS_WINDOWS, VS_X64, ONLY_MAKEFILES, SHOW_CPPS, VS_PROJ, TRACE, VS_PAR, VS_PAR_NUM
+- global DOTNET_ENABLED, DOTNET_KEY_FILE, JAVA_ENABLED, ML_ENABLED, STATIC_LIB, STATIC_BIN, PREFIX, GMP, FOCI2, FOCI2LIB, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH, GIT_DESCRIBE,
PYTHON_INSTALL_ENABLED, PYTHON_ENABLED
++ global DOTNET_ENABLED, DOTNET_KEY_FILE, JAVA_ENABLED, ML_ENABLED, STATIC_LIB, STATIC_BIN, PREFIX, DESTDIR, GMP, FOCI2, FOCI2LIB, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH, GIT_DESCRIBE,
PYTHON_INSTALL_ENABLED, PYTHON_ENABLED
+ global LINUX_X64, SLOW_OPTIMIZE, USE_OMP
+ try:
+ options, remainder = getopt.gnu_getopt(sys.argv[1:],
+ 'b:df:sxhmcvtnp:gj',
+ ['build=', 'debug', 'silent', 'x64', 'help', 'makefiles', 'showcpp', 'vsproj',
+- 'trace', 'dotnet', 'dotnet-key=', 'staticlib', 'prefix=', 'gmp', 'foci2=', 'java', 'parallel=', 'gprof',
++ 'trace', 'dotnet', 'dotnet-key=', 'staticlib', 'prefix=', 'destdir=', 'gmp', 'foci2=', 'java', 'parallel=', 'gprof',
+ 'githash=', 'git-describe', 'x86', 'ml', 'optimize', 'noomp', 'pypkgdir=', 'python', 'staticbin'])
+ except:
+ print("ERROR: Invalid command line option")
+@@ -727,6 +735,8 @@ def parse_options():
SLOW_OPTIMIZE = True
elif not IS_WINDOWS and opt in ('-p', '--prefix'):
PREFIX = arg
-- PYTHON_PACKAGE_DIR = os.path.join(PREFIX, 'lib', 'python%s' % distutils.sysconfig.get_python_version(), 'dist-packages')
-+ PYTHON_PACKAGE_DIR = os.path.join(PREFIX, 'lib', 'python%s' % distutils.sysconfig.get_python_version(), 'site-packages')
- mk_dir(DESTDIR + PYTHON_PACKAGE_DIR)
- if sys.version >= "3":
- mk_dir(os.path.join(DESTDIR + PYTHON_PACKAGE_DIR, '__pycache__'))
-@@ -1506,8 +1506,8 @@ class MLComponent(Component):
- get_component(Z3_DLL_COMPONENT).dll_name + '$(SO_EXT)',
- os.path.join(sub_dir, 'z3ml.cmxa'),
- os.path.join(sub_dir, 'META')))
-- out.write('\t%s remove Z3\n' % (OCAMLFIND))
-- out.write('\t%s install Z3 %s' % (OCAMLFIND, (os.path.join(sub_dir, 'META'))))
-+ out.write('\t%s remove -destdir $(DESTDIR)/ -ldconf ignore Z3\n' % (OCAMLFIND))
-+ out.write('\t%s install -destdir $(DESTDIR)/ -ldconf ignore Z3 %s' % (OCAMLFIND, (os.path.join(sub_dir, 'META'))))
- for m in modules:
- out.write(' %s.cma' % (os.path.join(sub_dir, m)))
Home |
Main Index |
Thread Index |
Old Index