pkgsrc-WIP-changes archive
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index][Old Index]
Package z3 version 4.5.0
Module Name: pkgsrc-wip
Committed By: Pierre Pronchery <khorben%defora.org@localhost>
Pushed By: khorben
Date: Fri Mar 9 13:55:24 2018 +0100
Changeset: 882312d8afc9b52c58b7f767e57b2b149ec7dc77
Modified Files:
Makefile
Added Files:
z3/DESCR
z3/Makefile
z3/PLIST
z3/buildlink3.mk
z3/distinfo
z3/options.mk
z3/patches/patch-configure
z3/patches/patch-scripts_mk__util.py
z3/patches/patch-src_util_stopwatch.h
Log Message:
Package z3 version 4.5.0
This was forked from z3 4.4.1 in math/z3.
I am creating a separate package for the Python bindings.
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.
To see a diff of this commit:
https://wip.pkgsrc.org/cgi-bin/gitweb.cgi?p=pkgsrc-wip.git;a=commitdiff;h=882312d8afc9b52c58b7f767e57b2b149ec7dc77
Please note that diffs are not public domain; they are subject to the
copyright notices on the relevant files.
diffstat:
Makefile | 1 +
z3/DESCR | 3 +
z3/Makefile | 24 ++++
z3/PLIST | 32 ++++++
z3/buildlink3.mk | 11 ++
z3/distinfo | 9 ++
z3/options.mk | 21 ++++
z3/patches/patch-configure | 12 ++
z3/patches/patch-scripts_mk__util.py | 209 ++++++++++++++++++++++++++++++++++
z3/patches/patch-src_util_stopwatch.h | 16 +++
10 files changed, 338 insertions(+)
diffs:
diff --git a/Makefile b/Makefile
index 5c5b347343..a39dd94f19 100644
--- a/Makefile
+++ b/Makefile
@@ -4703,6 +4703,7 @@ SUBDIR+= you-get
SUBDIR+= yp-tools
SUBDIR+= ypbind-mt
SUBDIR+= ypserv
+SUBDIR+= z3
SUBDIR+= zapping
SUBDIR+= zbackup
SUBDIR+= zbar
diff --git a/z3/DESCR b/z3/DESCR
new file mode 100644
index 0000000000..a15f33fa4e
--- /dev/null
+++ b/z3/DESCR
@@ -0,0 +1,3 @@
+z3 is an open source theorem prover / SMT solver from Microsoft Research.
+
+(SMT stands for "satisfiability modulo theories".)
diff --git a/z3/Makefile b/z3/Makefile
new file mode 100644
index 0000000000..4faa57558a
--- /dev/null
+++ b/z3/Makefile
@@ -0,0 +1,24 @@
+# $NetBSD: Makefile,v 1.7 2018/02/27 08:34:16 wiz Exp $
+
+DISTNAME= z3-4.5.0
+GITHUB_TAG= ${DISTNAME}
+CATEGORIES= math
+MASTER_SITES= ${MASTER_SITE_GITHUB:=Z3Prover/}
+
+MAINTAINER= dholland%NetBSD.org@localhost
+HOMEPAGE= https://github.com/Z3Prover/z3/
+COMMENT= The Z3 theorem prover / SMT solver
+LICENSE= mit
+
+WRKSRC= ${WRKDIR}/z3-${DISTNAME}
+HAS_CONFIGURE= yes
+USE_LANGUAGES= c c++
+BUILD_DIRS= build
+
+CONFIGURE_ENV+= PYTHON=${PYTHONBIN}
+CONFIGURE_ARGS+= --destdir=${DESTDIR} --prefix=${PREFIX}
+
+.include "options.mk"
+
+.include "../../lang/python/tool.mk"
+.include "../../mk/bsd.pkg.mk"
diff --git a/z3/PLIST b/z3/PLIST
new file mode 100644
index 0000000000..2070852aea
--- /dev/null
+++ b/z3/PLIST
@@ -0,0 +1,32 @@
+@comment $NetBSD$
+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
+${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 --git a/z3/buildlink3.mk b/z3/buildlink3.mk
new file mode 100644
index 0000000000..a17ce39723
--- /dev/null
+++ b/z3/buildlink3.mk
@@ -0,0 +1,11 @@
+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 --git a/z3/distinfo b/z3/distinfo
new file mode 100644
index 0000000000..3f8defa0ac
--- /dev/null
+++ b/z3/distinfo
@@ -0,0 +1,9 @@
+$NetBSD$
+
+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 --git a/z3/options.mk b/z3/options.mk
new file mode 100644
index 0000000000..ce802c00d8
--- /dev/null
+++ b/z3/options.mk
@@ -0,0 +1,21 @@
+# $NetBSD: options.mk,v 1.1 2015/11/24 05:45:58 dholland Exp $
+
+PKG_OPTIONS_VAR= PKG_OPTIONS.z3
+PKG_SUPPORTED_OPTIONS= ocaml java
+PKG_SUGGESTED_OPTIONS= ocaml
+
+.include "../../mk/bsd.options.mk"
+
+PLIST_VARS+= ocaml
+.if !empty(PKG_OPTIONS:Mocaml)
+CONFIGURE_ARGS+= --ml
+.include "../../lang/ocaml/buildlink3.mk"
+PLIST.ocaml= yes
+.endif
+
+.if !empty(PKG_OPTIONS:Mjava)
+# XXX untested
+USE_JAVA= yes
+CONFIGURE_ARGS+= --java
+.include "../../mk/java-vm.mk"
+.endif
diff --git a/z3/patches/patch-configure b/z3/patches/patch-configure
new file mode 100644
index 0000000000..e82f965aa8
--- /dev/null
+++ b/z3/patches/patch-configure
@@ -0,0 +1,12 @@
+$NetBSD$
+
+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 --git a/z3/patches/patch-scripts_mk__util.py b/z3/patches/patch-scripts_mk__util.py
new file mode 100644
index 0000000000..2ca5c95365
--- /dev/null
+++ b/z3/patches/patch-scripts_mk__util.py
@@ -0,0 +1,209 @@
+$NetBSD$
+
+--- scripts/mk_util.py.orig 2016-11-07 22:02:30.000000000 +0000
++++ scripts/mk_util.py
+@@ -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
++ elif not IS_WINDOWS and opt in ('-D', '--destdir'):
++ DESTDIR = arg
+ elif opt in ('--pypkgdir'):
+ PYTHON_PACKAGE_DIR = arg
+ elif IS_WINDOWS and opt == '--parallel':
+@@ -1208,9 +1218,9 @@ class ExeComponent(Component):
+
+ def mk_unix_dist(self, build_path, dist_path):
+ if self.install:
+- mk_dir(os.path.join(dist_path, INSTALL_BIN_DIR))
++ mk_dir(os.path.join(DESTDIR + dist_path, INSTALL_BIN_DIR))
+ shutil.copy(os.path.join(build_path, self.exe_name),
+- os.path.join(dist_path, INSTALL_BIN_DIR, self.exe_name))
++ os.path.join(DESTDIR + dist_path, INSTALL_BIN_DIR, self.exe_name))
+
+
+ class ExtraExeComponent(ExeComponent):
+@@ -1227,7 +1237,7 @@ def get_so_ext():
+ sysname = os.uname()[0]
+ if sysname == 'Darwin':
+ return 'dylib'
+- elif sysname == 'Linux' or sysname == 'FreeBSD' or sysname == 'OpenBSD':
++ elif sysname == 'Linux' or sysname == 'FreeBSD' or sysname == 'NetBSD' or sysname == 'OpenBSD':
+ return 'so'
+ elif sysname == 'CYGWIN':
+ return 'dll'
+@@ -1381,12 +1391,12 @@ class DLLComponent(Component):
+
+ def mk_unix_dist(self, build_path, dist_path):
+ if self.install:
+- mk_dir(os.path.join(dist_path, INSTALL_BIN_DIR))
++ mk_dir(os.path.join(DESTDIR + dist_path, INSTALL_BIN_DIR))
+ so = get_so_ext()
+ shutil.copy('%s.%s' % (os.path.join(build_path, self.dll_name), so),
+- '%s.%s' % (os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name), so))
++ '%s.%s' % (os.path.join(DESTDIR + dist_path, INSTALL_BIN_DIR, self.dll_name), so))
+ shutil.copy('%s.a' % os.path.join(build_path, self.dll_name),
+- '%s.a' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name))
++ '%s.a' % os.path.join(DESTDIR + dist_path, INSTALL_BIN_DIR, self.dll_name))
+
+ class PythonComponent(Component):
+ def __init__(self, name, libz3Component):
+@@ -1403,7 +1413,7 @@ class PythonComponent(Component):
+ return
+
+ src = os.path.join(build_path, 'python', 'z3')
+- dst = os.path.join(dist_path, INSTALL_BIN_DIR, 'python', 'z3')
++ dst = os.path.join(DESTDIR + dist_path, INSTALL_BIN_DIR, 'python', 'z3')
+ if os.path.exists(dst):
+ shutil.rmtree(dst)
+ shutil.copytree(src, dst)
+@@ -1701,11 +1711,11 @@ class DotNetDLLComponent(Component):
+
+ def mk_unix_dist(self, build_path, dist_path):
+ if is_dotnet_enabled():
+- mk_dir(os.path.join(dist_path, INSTALL_BIN_DIR))
++ mk_dir(os.path.join(DESTDIR + dist_path, INSTALL_BIN_DIR))
+ shutil.copy('%s.dll' % os.path.join(build_path, self.dll_name),
+- '%s.dll' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name))
++ '%s.dll' % os.path.join(DESTDIR + dist_path, INSTALL_BIN_DIR, self.dll_name))
+ shutil.copy('%s.xml' % os.path.join(build_path, self.dll_name),
+- '%s.xml' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name))
++ '%s.xml' % os.path.join(DESTDIR + dist_path, INSTALL_BIN_DIR, self.dll_name))
+
+ def mk_install_deps(self, out):
+ if not is_dotnet_enabled():
+@@ -1776,6 +1786,8 @@ class JavaDLLComponent(Component):
+ t = t.replace('PLATFORM', 'linux')
+ elif IS_FREEBSD:
+ t = t.replace('PLATFORM', 'freebsd')
++ elif IS_NETBSD:
++ t = t.replace('PLATFORM', 'netbsd')
+ elif IS_OPENBSD:
+ t = t.replace('PLATFORM', 'openbsd')
+ elif IS_CYGWIN:
+@@ -1827,12 +1839,12 @@ class JavaDLLComponent(Component):
+
+ def mk_unix_dist(self, build_path, dist_path):
+ if JAVA_ENABLED:
+- mk_dir(os.path.join(dist_path, INSTALL_BIN_DIR))
++ mk_dir(os.path.join(DESTDIR + dist_path, INSTALL_BIN_DIR))
+ shutil.copy('%s.jar' % os.path.join(build_path, self.package_name),
+- '%s.jar' % os.path.join(dist_path, INSTALL_BIN_DIR, self.package_name))
++ '%s.jar' % os.path.join(DESTDIR + dist_path, INSTALL_BIN_DIR, self.package_name))
+ so = get_so_ext()
+ shutil.copy(os.path.join(build_path, 'libz3java.%s' % so),
+- os.path.join(dist_path, INSTALL_BIN_DIR, 'libz3java.%s' % so))
++ os.path.join(DESTDIR + dist_path, INSTALL_BIN_DIR, 'libz3java.%s' % so))
+
+ def mk_install(self, out):
+ if is_java_enabled() and self.install:
+@@ -2451,6 +2463,13 @@ def mk_config():
+ LDFLAGS = '%s -lrt' % LDFLAGS
+ SLIBFLAGS = '-shared'
+ SLIBEXTRAFLAGS = '%s -lrt' % SLIBEXTRAFLAGS
++ elif sysname == 'NetBSD':
++ CXXFLAGS = '%s -fno-strict-aliasing -D_NETBSD_' % CXXFLAGS
++ OS_DEFINES = '-D_NETBSD_'
++ SO_EXT = '.so'
++ LDFLAGS = '%s -lrt' % LDFLAGS
++ SLIBFLAGS = '-shared'
++ SLIBEXTRAFLAGS = '%s -lrt' % SLIBEXTRAFLAGS
+ elif sysname == 'OpenBSD':
+ CXXFLAGS = '%s -fno-strict-aliasing -D_OPENBSD_' % CXXFLAGS
+ OS_DEFINES = '-D_OPENBSD_'
+@@ -2486,6 +2505,7 @@ def mk_config():
+ LDFLAGS = '%s -static-libgcc -static-libstdc++' % LDFLAGS
+
+ config.write('PREFIX=%s\n' % PREFIX)
++ config.write('DESTDIR=%s\n' % DESTDIR)
+ config.write('CC=%s\n' % CC)
+ config.write('CXX=%s\n' % CXX)
+ config.write('CXXFLAGS=%s %s\n' % (CPPFLAGS, CXXFLAGS))
+@@ -2520,6 +2540,7 @@ def mk_config():
+ print('Arithmetic: %s' % ARITH)
+ print('OpenMP: %s' % HAS_OMP)
+ print('Prefix: %s' % PREFIX)
++ print('Destdir: %s' % DESTDIR)
+ print('64-bit: %s' % is64())
+ print('FP math: %s' % FPMATH)
+ print("Python pkg dir: %s" % PYTHON_PACKAGE_DIR)
+@@ -2580,7 +2601,10 @@ def mk_makefile():
+ pathvar = "DYLD_LIBRARY_PATH" if IS_OSX else "PATH" if IS_WINDOWS else "LD_LIBRARY_PATH"
+ out.write("\t@echo \"Z3Py scripts stored in arbitrary directories can be executed if the \'%s\' directory is added to the PYTHONPATH environment variable and the \'%s\' directory is added to the %s environment variable.\"\n" % (os.path.join(BUILD_DIR, 'python'), BUILD_DIR, pathvar))
+ if not IS_WINDOWS:
+- out.write("\t@echo Use the following command to install Z3 at prefix $(PREFIX).\n")
++ out.write("\t@echo Use the following command to install Z3 at prefix $(PREFIX)")
++ if DESTDIR != "":
++ out.write(" under destdir $(DESTDIR)")
++ out.write(".\n")
+ out.write('\t@echo " sudo make install"\n\n')
+ # out.write("\t@echo If you are doing a staged install you can use DESTDIR.\n")
+ # out.write('\t@echo " make DESTDIR=/some/temp/directory install"\n')
+@@ -3283,7 +3307,7 @@ def mk_unix_dist(build_path, dist_path):
+ # Add Z3Py to bin directory
+ for pyc in filter(lambda f: f.endswith('.pyc') or f.endswith('.py'), os.listdir(build_path)):
+ shutil.copy(os.path.join(build_path, pyc),
+- os.path.join(dist_path, INSTALL_BIN_DIR, pyc))
++ os.path.join(DESTDIR + dist_path, INSTALL_BIN_DIR, pyc))
+
+ class MakeRuleCmd(object):
+ """
diff --git a/z3/patches/patch-src_util_stopwatch.h b/z3/patches/patch-src_util_stopwatch.h
new file mode 100644
index 0000000000..729e9b3b7b
--- /dev/null
+++ b/z3/patches/patch-src_util_stopwatch.h
@@ -0,0 +1,16 @@
+$NetBSD$
+
+--- src/util/stopwatch.h.orig 2016-11-07 22:02:30.000000000 +0000
++++ src/util/stopwatch.h
+@@ -130,6 +130,11 @@ public:
+
+ #include<ctime>
+
++#ifndef CLOCK_PROCESS_CPUTIME_ID
++/* BSD */
++# define CLOCK_PROCESS_CPUTIME_ID CLOCK_MONOTONIC
++#endif
++
+ class stopwatch {
+ unsigned long long m_time; // elapsed time in ns
+ bool m_running;
Home |
Main Index |
Thread Index |
Old Index