Make python stuff live in a python directory in the build tree

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')

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):
+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)
+    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)
+    mk_dir(z3py_dest)
-    shutil.copytree(z3py_src, z3py_dest)
+    for py in filter(lambda f: f.endswith('.py'), os.listdir(z3py_src)):
-    if is_verbose():
+        shutil.copyfile(os.path.join(z3py_src, py), os.path.join(z3py_dest, py))
-        print("Copied python bindings")
+        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:

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:
+  if _lib is None:
-    _dir = pkg_resources.resource_filename('z3', 'lib')
+    _dirs = ['.', pkg_resources.resource_filename('z3', 'lib'), os.path.join(sys.prefix, 'lib'), '']
-    for ext in ['dll', 'so', 'dylib']:
+    for _dir in _dirs:
       try:
-        init(os.path.join(_dir, 'libz3.%s' % ext))
+        init(_dir)
         break
       except:
         pass
-      try:
+    if _lib is None:
-        init('libz3.%s' % ext)
-        break
-      except:
-        pass
-    if _lib == 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)
 """