File python-use-non-devel-so.patch of Package z3
From: https://github.com/sertonix
Patch-mainline: submitted https://github.com/Z3Prover/z3/issues/7518
Subject: Use sover for python bindings
Don't use libz3.so, but use versioned lib like libz3.so.4.15.0
---
scripts/update_api.py | 33 +++++++++++++++++++++++++--------
src/api/python/CMakeLists.txt | 2 ++
2 files changed, 27 insertions(+), 8 deletions(-)
--- a/scripts/update_api.py
+++ b/scripts/update_api.py
@@ -1823,9 +1823,10 @@ del _lib
del _default_dirs
del _all_dirs
del _ext
+del _sover
""")
-def write_core_py_preamble(core_py):
+def write_core_py_preamble(core_py, z3py_soversion):
core_py.write(
"""
# Automatically generated file
@@ -1842,6 +1843,11 @@ from .z3consts import *
_file_manager = contextlib.ExitStack()
atexit.register(_file_manager.close)
+"""
+ )
+ core_py.write("_sover=\"%s\"\n" % z3py_soversion)
+ core_py.write(
+"""
_ext = 'dll' if sys.platform in ('win32', 'cygwin') else 'dylib' if sys.platform == 'darwin' else 'so'
_lib = None
_z3_lib_resource = importlib_resources.files('z3').joinpath('lib')
@@ -1877,7 +1883,7 @@ for d in _all_dirs:
try:
d = os.path.realpath(d)
if os.path.isdir(d):
- d = os.path.join(d, 'libz3.%s' % _ext)
+ d = os.path.join(d, 'libz3.%s.%s' % (_ext, _sover))
if os.path.isfile(d):
_lib = ctypes.CDLL(d)
break
@@ -1888,24 +1894,24 @@ for d in _all_dirs:
if _lib is None:
# If all else failed, ask the system to find it.
try:
- _lib = ctypes.CDLL('libz3.%s' % _ext)
+ _lib = ctypes.CDLL('libz3.%s.%s' % (_ext, _sover))
except Exception as e:
_failures += [e]
pass
if _lib is None:
- print("Could not find libz3.%s; consider adding the directory containing it to" % _ext)
+ print("Could not find libz3.%s.%s; consider adding the directory containing it to" % (_ext, _sover))
print(" - your system's PATH environment variable,")
print(" - the Z3_LIBRARY_PATH environment variable, or ")
print(" - to the custom Z3_LIB_DIRS Python-builtin before importing the z3 module, e.g. via")
if sys.version < '3':
print(" import __builtin__")
- print(" __builtin__.Z3_LIB_DIRS = [ '/path/to/z3/lib/dir' ] # directory containing libz3.%s" % _ext)
+ print(" __builtin__.Z3_LIB_DIRS = [ '/path/to/z3/lib/dir' ] # directory containing libz3.%s.%s" % (_ext, _sover))
else:
print(" import builtins")
- print(" builtins.Z3_LIB_DIRS = [ '/path/to/z3/lib/dir' ] # directory containing libz3.%s" % _ext)
+ print(" builtins.Z3_LIB_DIRS = [ '/path/to/z3/lib/dir' ] # directory containing libz3.%s.%s" % (_ext, _sover))
print(_failures)
- raise Z3Exception("libz3.%s not found." % _ext)
+ raise Z3Exception("libz3.%s.%s not found." % (_ext, _sover))
if sys.version < '3':
@@ -1970,6 +1976,7 @@ core_py = None
def generate_files(api_files,
api_output_dir=None,
z3py_output_dir=None,
+ z3py_soversion=None,
dotnet_output_dir=None,
java_input_dir=None,
java_output_dir=None,
@@ -2026,7 +2033,7 @@ def generate_files(api_files,
write_log_h_preamble(log_h)
write_log_c_preamble(log_c)
write_exe_c_preamble(exe_c)
- write_core_py_preamble(core_py)
+ write_core_py_preamble(core_py, z3py_soversion)
# FIXME: these functions are awful
apiTypes.def_Types(api_files)
@@ -2069,6 +2076,10 @@ def main(args):
dest="z3py_output_dir",
default=None,
help="Directory to emit z3py files. If not specified no files are emitted.")
+ parser.add_argument("--z3py-soversion",
+ dest="z3py_soversion",
+ default=None,
+ help="SOVERSION for loading libz3 library.")
parser.add_argument("--dotnet-output-dir",
dest="dotnet_output_dir",
default=None,
@@ -2095,6 +2106,11 @@ def main(args):
help="Directory to emit OCaml files. If not specified no files are emitted.")
pargs = parser.parse_args(args)
+ if pargs.z3py_output_dir:
+ if pargs.z3py_soversion is None:
+ logging.error('--z3py-soversion must be specified')
+ return 1
+
if pargs.java_output_dir:
if pargs.java_package_name == None:
logging.error('--java-package-name must be specified')
@@ -2116,6 +2132,7 @@ def main(args):
generate_files(api_files=pargs.api_files,
api_output_dir=pargs.api_output_dir,
z3py_output_dir=pargs.z3py_output_dir,
+ z3py_soversion=pargs.z3py_soversion,
dotnet_output_dir=pargs.dotnet_output_dir,
java_input_dir=pargs.java_input_dir,
java_output_dir=pargs.java_output_dir,
--- a/src/api/python/CMakeLists.txt
+++ b/src/api/python/CMakeLists.txt
@@ -36,6 +36,8 @@ add_custom_command(OUTPUT "${z3py_bindin
COMMAND "${Python3_EXECUTABLE}"
"${PROJECT_SOURCE_DIR}/scripts/update_api.py"
${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
+ "--z3py-soversion"
+ ${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR}
"--z3py-output-dir"
"${z3py_bindings_build_dest}"
DEPENDS
