From cb83c42100e7fc1a2bbf7182523b9e19cda53bdf Mon Sep 17 00:00:00 2001 From: Andrew Dutcher Date: Sat, 10 Sep 2016 11:41:04 -0700 Subject: [PATCH] Make python stuff live in a python directory in the build tree --- scripts/mk_project.py | 3 +- scripts/mk_util.py | 75 +++++++++++++++++++++++++------------------ scripts/update_api.py | 21 ++++++------ 3 files changed, 56 insertions(+), 43 deletions(-) diff --git a/scripts/mk_project.py b/scripts/mk_project.py index 78bc290f8..00b5cdef5 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -87,7 +87,8 @@ def init_project_def(): reexports=['api'], dll_name='libz3', static=build_static_lib(), - export_files=API_files) + export_files=API_files, + staging_link='python') add_dot_net_dll('dotnet', ['api_dll'], 'api/dotnet', dll_name='Microsoft.Z3', assembly_info_dir='Properties', default_key_file='src/api/dotnet/Microsoft.Z3.snk') add_java_dll('java', ['api_dll'], 'api/java', dll_name='libz3java', package_name="com.microsoft.z3", manifest_file='manifest') add_ml_lib('ml', ['api_dll'], 'api/ml', lib_name='libz3ml') diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 0d2b23a3e..eca0c4738 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -1230,7 +1230,7 @@ def get_so_ext(): return 'dll' class DLLComponent(Component): - def __init__(self, name, dll_name, path, deps, export_files, reexports, install, static): + def __init__(self, name, dll_name, path, deps, export_files, reexports, install, static, staging_link=None): Component.__init__(self, name, path, deps) if dll_name is None: dll_name = name @@ -1239,6 +1239,7 @@ class DLLComponent(Component): self.reexports = reexports self.install = install self.static = static + self.staging_link = staging_link # link a copy of the shared object into this directory on build def get_link_name(self): if self.static: @@ -1294,6 +1295,11 @@ class DLLComponent(Component): out.write(' $(SLINK_EXTRA_FLAGS)') if IS_WINDOWS: out.write(' /DEF:%s.def' % os.path.join(self.to_src_dir, self.name)) + if self.staging_link: + if IS_WINDOWS or IS_OSX: + out.write('\n\tcp %s %s' % (self.dll_file(), self.staging_link)) + else: + out.write('\n\tln -s %s %s' % (os.path.join(reverse_path(self.staging_link), self.dll_file()), self.staging_link)) out.write('\n') if self.static: if IS_WINDOWS: @@ -1432,13 +1438,18 @@ class PythonInstallComponent(Component): def mk_install(self, out): if not is_python_install_enabled(): return - MakeRuleCmd.make_install_directory(out, self.pythonPkgDir, in_prefix=self.in_prefix_install) + MakeRuleCmd.make_install_directory(out, + os.path.join(self.pythonPkgDir, 'z3'), + in_prefix=self.in_prefix_install) + MakeRuleCmd.make_install_directory(out, + os.path.join(self.pythonPkgDir, 'z3', 'lib'), + in_prefix=self.in_prefix_install) # Sym-link or copy libz3 into python package directory if IS_WINDOWS or IS_OSX: MakeRuleCmd.install_files(out, self.libz3Component.dll_file(), - os.path.join(self.pythonPkgDir, + os.path.join(self.pythonPkgDir, 'z3', 'lib', self.libz3Component.dll_file()), in_prefix=self.in_prefix_install ) @@ -1449,34 +1460,29 @@ class PythonInstallComponent(Component): # staged installs that use DESTDIR). MakeRuleCmd.create_relative_symbolic_link(out, self.libz3Component.install_path(), - os.path.join(self.pythonPkgDir, + os.path.join(self.pythonPkgDir, 'z3', 'lib', self.libz3Component.dll_file() ), ) - MakeRuleCmd.install_files(out, 'z3*.py', self.pythonPkgDir, + MakeRuleCmd.install_files(out, os.path.join('python', 'z3', '*.py'), + os.path.join(self.pythonPkgDir, 'z3'), in_prefix=self.in_prefix_install) if sys.version >= "3": - pythonPycacheDir = os.path.join(self.pythonPkgDir, '__pycache__') + pythonPycacheDir = os.path.join(self.pythonPkgDir, 'z3', '__pycache__') MakeRuleCmd.make_install_directory(out, pythonPycacheDir, in_prefix=self.in_prefix_install) MakeRuleCmd.install_files(out, - '{}*.pyc'.format(os.path.join('__pycache__', 'z3')), + os.path.join('python', 'z3', '__pycache__', '*.pyc'), pythonPycacheDir, in_prefix=self.in_prefix_install) else: MakeRuleCmd.install_files(out, - 'z3*.pyc', + os.path.join('python', 'z3', '*.pyc'), self.pythonPkgDir, in_prefix=self.in_prefix_install) if PYTHON_PACKAGE_DIR != distutils.sysconfig.get_python_lib(): - if os.uname()[0] == 'Darwin': - LD_LIBRARY_PATH = "DYLD_LIBRARY_PATH" - else: - LD_LIBRARY_PATH = "LD_LIBRARY_PATH" - out.write('\t@echo Z3 shared libraries were installed at \'%s\', make sure this directory is in your %s environment variable.\n' % - (os.path.join(PREFIX, INSTALL_LIB_DIR), LD_LIBRARY_PATH)) out.write('\t@echo Z3Py was installed at \'%s\', make sure this directory is in your PYTHONPATH environment variable.' % PYTHON_PACKAGE_DIR) def mk_uninstall(self, out): @@ -1488,13 +1494,13 @@ class PythonInstallComponent(Component): in_prefix=self.in_prefix_install ) MakeRuleCmd.remove_installed_files(out, - '{}*.py'.format(os.path.join(self.pythonPkgDir, 'z3')), + os.path.join(self.pythonPkgDir, 'z3', '*.py'), in_prefix=self.in_prefix_install) MakeRuleCmd.remove_installed_files(out, - '{}*.pyc'.format(os.path.join(self.pythonPkgDir, 'z3')), + os.path.join(self.pythonPkgDir, 'z3', '*.pyc'), in_prefix=self.in_prefix_install) MakeRuleCmd.remove_installed_files(out, - '{}*.pyc'.format(os.path.join(self.pythonPkgDir, '__pycache__', 'z3')), + os.path.join(self.pythonPkgDir, 'z3', '__pycache__', '*.pyc'), in_prefix=self.in_prefix_install ) @@ -2157,9 +2163,9 @@ class PythonExampleComponent(ExampleComponent): def mk_makefile(self, out): full = os.path.join(EXAMPLE_DIR, self.path) for py in filter(lambda f: f.endswith('.py'), os.listdir(full)): - shutil.copyfile(os.path.join(full, py), os.path.join(BUILD_DIR, py)) + shutil.copyfile(os.path.join(full, py), os.path.join(BUILD_DIR, 'python', py)) if is_verbose(): - print("Copied Z3Py example '%s' to '%s'" % (py, BUILD_DIR)) + print("Copied Z3Py example '%s' to '%s'" % (py, os.path.join(BUILD_DIR, 'python'))) out.write('_ex_%s: \n\n' % self.name) @@ -2189,8 +2195,8 @@ def add_extra_exe(name, deps=[], path=None, exe_name=None, install=True): c = ExtraExeComponent(name, exe_name, path, deps, install) reg_component(name, c) -def add_dll(name, deps=[], path=None, dll_name=None, export_files=[], reexports=[], install=True, static=False): - c = DLLComponent(name, dll_name, path, deps, export_files, reexports, install, static) +def add_dll(name, deps=[], path=None, dll_name=None, export_files=[], reexports=[], install=True, static=False, staging_link=None): + c = DLLComponent(name, dll_name, path, deps, export_files, reexports, install, static, staging_link) reg_component(name, c) return c @@ -2519,9 +2525,9 @@ def mk_makefile(): if c.main_component(): out.write(' %s' % c.name) out.write('\n\t@echo Z3 was successfully built.\n') - out.write("\t@echo \"Z3Py scripts can already be executed in the \'%s\' directory.\"\n" % BUILD_DIR) + out.write("\t@echo \"Z3Py scripts can already be executed in the \'%s\' directory.\"\n" % os.path.join(BUILD_DIR, 'python')) 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 and %s environment variables.\"\n" % (BUILD_DIR, pathvar)) + 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 " sudo make install"\n\n') @@ -2737,35 +2743,40 @@ def mk_def_files(): def cp_z3py_to_build(): mk_dir(BUILD_DIR) - z3py_dest = os.path.join(BUILD_DIR, 'z3.py') + mk_dir(os.path.join(BUILD_DIR, 'python')) + z3py_dest = os.path.join(BUILD_DIR, 'python', 'z3') z3py_src = os.path.join(Z3PY_SRC_DIR, 'z3') + # Erase existing .pyc files for root, dirs, files in os.walk(Z3PY_SRC_DIR): for f in files: if f.endswith('.pyc'): rmf(os.path.join(root, f)) # Compile Z3Py files - if compileall.compile_dir(Z3PY_SRC_DIR, force=1) != 1: + if compileall.compile_dir(z3py_src, force=1) != 1: raise MKException("failed to compile Z3Py sources") + if is_verbose: + print("Generated python bytecode") # Copy sources to build - shutil.rmtree(z3py_dest, ignore_errors=True) - shutil.copytree(z3py_src, z3py_dest) - if is_verbose(): - print("Copied python bindings") + mk_dir(z3py_dest) + for py in filter(lambda f: f.endswith('.py'), os.listdir(z3py_src)): + shutil.copyfile(os.path.join(z3py_src, py), os.path.join(z3py_dest, py)) + if is_verbose(): + print("Copied '%s'" % py) # Python 2.x support for pyc in filter(lambda f: f.endswith('.pyc'), os.listdir(z3py_src)): shutil.copyfile(os.path.join(z3py_src, pyc), os.path.join(z3py_dest, pyc)) if is_verbose(): - print("Generated '%s'" % pyc) + print("Copied '%s'" % pyc) # Python 3.x support src_pycache = os.path.join(z3py_src, '__pycache__') + target_pycache = os.path.join(z3py_dest, '__pycache__') if os.path.exists(src_pycache): for pyc in filter(lambda f: f.endswith('.pyc'), os.listdir(src_pycache)): - target_pycache = os.path.join(z3py_dest, '__pycache__') mk_dir(target_pycache) shutil.copyfile(os.path.join(src_pycache, pyc), os.path.join(target_pycache, pyc)) if is_verbose(): - print("Generated '%s'" % pyc) + print("Copied '%s'" % pyc) def mk_bindings(api_files): if not ONLY_MAKEFILES: diff --git a/scripts/update_api.py b/scripts/update_api.py index 1f0ae4e4c..48a4d6114 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -1605,23 +1605,20 @@ def write_core_py_preamble(core_py): core_py.write('from .z3consts import *\n') core_py.write( """ +_ext = 'dll' if sys.platform in ('win32', 'cygwin') else 'dylib' if sys.platform == 'darwin' else 'so' + _lib = None def lib(): global _lib - if _lib == None: - _dir = pkg_resources.resource_filename('z3', 'lib') - for ext in ['dll', 'so', 'dylib']: + if _lib is None: + _dirs = ['.', pkg_resources.resource_filename('z3', 'lib'), os.path.join(sys.prefix, 'lib'), ''] + for _dir in _dirs: try: - init(os.path.join(_dir, 'libz3.%s' % ext)) + init(_dir) break except: pass - try: - init('libz3.%s' % ext) - break - except: - pass - if _lib == None: + if _lib is None: raise Z3Exception("init(Z3_LIBRARY_PATH) must be invoked before using Z3-python") return _lib @@ -1644,6 +1641,10 @@ else: return "" def init(PATH): + PATH = os.path.realpath(PATH) + if os.path.isdir(PATH): + PATH = os.path.join(PATH, 'libz3.%s' % _ext) + global _lib _lib = ctypes.CDLL(PATH) """