From 9489665ddcc35dc99fc0367ab073ba15d9854043 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Mon, 23 Nov 2015 22:47:46 +0000
Subject: [PATCH 01/15] Partially fix not being able to do a staged package
 install of Z3 using the DESTDIR make file variable
 (https://www.gnu.org/prep/standards/html_node/DESTDIR.html) for ``install``
 and ``uninstall`` targets.

Typically packagers build packages like so

```
$ ./configure --prefix=/usr/
$ make
$ make DESTDIR=/some/path/ install
```

Doing this installs the files into a directory ``/some/path`` but places
files inside that directory using the layout in ``--prefix`` (e.g.
``/some/path/usr/bin/z3``).  The ``/some/path`` directory can then be
packaged (e.g. tarballed) for later installation.

The ``DESTDIR`` is not set in the Makefile and thus is empty by default
which maintains the existing ``make install`` behaviour.

Unfortunately this situation isn't fixed for the Python bindings (and
possibly others) yet as more invasive changes are needed here. I'll fix
this in later commits.
---
 scripts/mk_util.py | 22 +++++++++++-----------
 1 file changed, 11 insertions(+), 11 deletions(-)

diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 83669472d..0a3745a2f 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -992,11 +992,11 @@ class LibComponent(Component):
 
     def mk_install(self, out):
         for include in self.includes2install:
-            out.write('\t@cp %s %s\n' % (os.path.join(self.to_src_dir, include), os.path.join('$(PREFIX)', 'include', include)))
+            out.write('\t@cp %s %s\n' % (os.path.join(self.to_src_dir, include), os.path.join('$(DESTDIR)$(PREFIX)', 'include', include)))
 
     def mk_uninstall(self, out):
         for include in self.includes2install:
-            out.write('\t@rm -f %s\n' % os.path.join('$(PREFIX)', 'include', include))
+            out.write('\t@rm -f %s\n' % os.path.join('$(DESTDIR)$(PREFIX)', 'include', include))
 
     def mk_win_dist(self, build_path, dist_path):
         mk_dir(os.path.join(dist_path, 'include'))
@@ -1078,11 +1078,11 @@ class ExeComponent(Component):
     def mk_install(self, out):
         if self.install:
             exefile = '%s$(EXE_EXT)' % self.exe_name
-            out.write('\t@cp %s %s\n' % (exefile, os.path.join('$(PREFIX)', 'bin', exefile)))
+            out.write('\t@cp %s %s\n' % (exefile, os.path.join('$(DESTDIR)$(PREFIX)', 'bin', exefile)))
 
     def mk_uninstall(self, out):
         exefile = '%s$(EXE_EXT)' % self.exe_name
-        out.write('\t@rm -f %s\n' % os.path.join('$(PREFIX)', 'bin', exefile))
+        out.write('\t@rm -f %s\n' % os.path.join('$(DESTDIR)$(PREFIX)', 'bin', exefile))
 
     def mk_win_dist(self, build_path, dist_path):
         if self.install:
@@ -1224,19 +1224,19 @@ class DLLComponent(Component):
     def mk_install(self, out):
         if self.install:
             dllfile = '%s$(SO_EXT)' % self.dll_name
-            out.write('\t@cp %s %s\n' % (dllfile, os.path.join('$(PREFIX)', 'lib', dllfile)))
+            out.write('\t@cp %s %s\n' % (dllfile, os.path.join('$(DESTDIR)$(PREFIX)', 'lib', dllfile)))
             out.write('\t@cp %s %s\n' % (dllfile, os.path.join(PYTHON_PACKAGE_DIR, dllfile)))
             if self.static:
                 libfile = '%s$(LIB_EXT)' % self.dll_name
-                out.write('\t@cp %s %s\n' % (libfile, os.path.join('$(PREFIX)', 'lib', libfile)))
+                out.write('\t@cp %s %s\n' % (libfile, os.path.join('$(DESTDIR)$(PREFIX)', 'lib', libfile)))
 
 
     def mk_uninstall(self, out):
         dllfile = '%s$(SO_EXT)' % self.dll_name
-        out.write('\t@rm -f %s\n' % os.path.join('$(PREFIX)', 'lib', dllfile))
+        out.write('\t@rm -f %s\n' % os.path.join('$(DESTDIR)$(PREFIX)', 'lib', dllfile))
         out.write('\t@rm -f %s\n' % os.path.join(PYTHON_PACKAGE_DIR, dllfile))
         libfile = '%s$(LIB_EXT)' % self.dll_name
-        out.write('\t@rm -f %s\n' % os.path.join('$(PREFIX)', 'lib', libfile))
+        out.write('\t@rm -f %s\n' % os.path.join('$(DESTDIR)$(PREFIX)', 'lib', libfile))
 
     def mk_win_dist(self, build_path, dist_path):
         if self.install:
@@ -2009,9 +2009,9 @@ def mk_install(out):
     if is_ml_enabled() and OCAMLFIND != '':
         out.write('ocamlfind_install')
     out.write('\n')
-    out.write('\t@mkdir -p %s\n' % os.path.join('$(PREFIX)', 'bin'))
-    out.write('\t@mkdir -p %s\n' % os.path.join('$(PREFIX)', 'include'))
-    out.write('\t@mkdir -p %s\n' % os.path.join('$(PREFIX)', 'lib'))
+    out.write('\t@mkdir -p %s\n' % os.path.join('$(DESTDIR)$(PREFIX)', 'bin'))
+    out.write('\t@mkdir -p %s\n' % os.path.join('$(DESTDIR)$(PREFIX)', 'include'))
+    out.write('\t@mkdir -p %s\n' % os.path.join('$(DESTDIR)$(PREFIX)', 'lib'))
     for c in get_components():
         c.mk_install(out)
     out.write('\t@cp z3*.py %s\n' % PYTHON_PACKAGE_DIR)

From b285ce7ceeba659596feb66aacf1140fc7abbc71 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Tue, 24 Nov 2015 09:14:08 +0000
Subject: [PATCH 02/15] Partially fix not being able to do a staged install
 (using ``DESTDIR``) when installing the Python bindings.

If ``DESTDIR`` is set the bindings will now be installed under this
path but ``$(PREFIX)`` only appears in the ``Makefile`` if ``--prefix``
was set which seems a little broken (we'll fix this soon).

The creation of the Python ``site-packages`` (and ``__pycache__`` for Python
3) directories has been moved to build time instead of configure time
because we don't know what ``DESTDIR`` will be set to at configure time.
---
 scripts/mk_util.py | 23 +++++++++++------------
 1 file changed, 11 insertions(+), 12 deletions(-)

diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 0a3745a2f..0cad588dc 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -637,10 +637,7 @@ 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')
-            mk_dir(PYTHON_PACKAGE_DIR)
-            if sys.version >= "3":
-                mk_dir(os.path.join(PYTHON_PACKAGE_DIR, '__pycache__'))
+            PYTHON_PACKAGE_DIR = os.path.join('$(PREFIX)', 'lib', 'python%s' % distutils.sysconfig.get_python_version(), 'dist-packages')
         elif IS_WINDOWS and opt == '--parallel':
             VS_PAR = True
             VS_PAR_NUM = int(arg)
@@ -1225,7 +1222,7 @@ class DLLComponent(Component):
         if self.install:
             dllfile = '%s$(SO_EXT)' % self.dll_name
             out.write('\t@cp %s %s\n' % (dllfile, os.path.join('$(DESTDIR)$(PREFIX)', 'lib', dllfile)))
-            out.write('\t@cp %s %s\n' % (dllfile, os.path.join(PYTHON_PACKAGE_DIR, dllfile)))
+            out.write('\t@cp %s $(DESTDIR)%s\n' % (dllfile, os.path.join(PYTHON_PACKAGE_DIR, dllfile)))
             if self.static:
                 libfile = '%s$(LIB_EXT)' % self.dll_name
                 out.write('\t@cp %s %s\n' % (libfile, os.path.join('$(DESTDIR)$(PREFIX)', 'lib', libfile)))
@@ -1234,7 +1231,7 @@ class DLLComponent(Component):
     def mk_uninstall(self, out):
         dllfile = '%s$(SO_EXT)' % self.dll_name
         out.write('\t@rm -f %s\n' % os.path.join('$(DESTDIR)$(PREFIX)', 'lib', dllfile))
-        out.write('\t@rm -f %s\n' % os.path.join(PYTHON_PACKAGE_DIR, dllfile))
+        out.write('\t@rm -f $(DESTDIR)%s\n' % os.path.join(PYTHON_PACKAGE_DIR, dllfile))
         libfile = '%s$(LIB_EXT)' % self.dll_name
         out.write('\t@rm -f %s\n' % os.path.join('$(DESTDIR)$(PREFIX)', 'lib', libfile))
 
@@ -2012,14 +2009,16 @@ def mk_install(out):
     out.write('\t@mkdir -p %s\n' % os.path.join('$(DESTDIR)$(PREFIX)', 'bin'))
     out.write('\t@mkdir -p %s\n' % os.path.join('$(DESTDIR)$(PREFIX)', 'include'))
     out.write('\t@mkdir -p %s\n' % os.path.join('$(DESTDIR)$(PREFIX)', 'lib'))
+    out.write('\t@mkdir -p $(DESTDIR)%s\n' % PYTHON_PACKAGE_DIR)
     for c in get_components():
         c.mk_install(out)
-    out.write('\t@cp z3*.py %s\n' % PYTHON_PACKAGE_DIR)
+    out.write('\t@cp z3*.py $(DESTDIR)%s\n' % PYTHON_PACKAGE_DIR)
     if sys.version >= "3":
-        out.write('\t@cp %s*.pyc %s\n' % (os.path.join('__pycache__', 'z3'),
+        out.write('\t@mkdir -p $(DESTDIR)%s\n' % os.path.join(PYTHON_PACKAGE_DIR, '__pycache__'))
+        out.write('\t@cp %s*.pyc $(DESTDIR)%s\n' % (os.path.join('__pycache__', 'z3'),
                                           os.path.join(PYTHON_PACKAGE_DIR, '__pycache__')))
     else:
-        out.write('\t@cp z3*.pyc %s\n' % PYTHON_PACKAGE_DIR)
+        out.write('\t@cp z3*.pyc $(DESTDIR)%s\n' % PYTHON_PACKAGE_DIR)
     out.write('\t@echo Z3 was successfully installed.\n')
     if PYTHON_PACKAGE_DIR != distutils.sysconfig.get_python_lib():
         if os.uname()[0] == 'Darwin':
@@ -2035,9 +2034,9 @@ def mk_uninstall(out):
     out.write('uninstall:\n')
     for c in get_components():
         c.mk_uninstall(out)
-    out.write('\t@rm -f %s*.py\n' % os.path.join(PYTHON_PACKAGE_DIR, 'z3'))
-    out.write('\t@rm -f %s*.pyc\n' % os.path.join(PYTHON_PACKAGE_DIR, 'z3'))
-    out.write('\t@rm -f %s*.pyc\n' % os.path.join(PYTHON_PACKAGE_DIR, '__pycache__', 'z3'))
+    out.write('\t@rm -f $(DESTDIR)%s*.py\n' % os.path.join(PYTHON_PACKAGE_DIR, 'z3'))
+    out.write('\t@rm -f $(DESTDIR)%s*.pyc\n' % os.path.join(PYTHON_PACKAGE_DIR, 'z3'))
+    out.write('\t@rm -f $(DESTDIR)%s*.pyc\n' % os.path.join(PYTHON_PACKAGE_DIR, '__pycache__', 'z3'))
     out.write('\t@echo Z3 was successfully uninstalled.\n')
     out.write('\n')
 

From 4c11037d70db1ef8c533395cf298aaf1e1505255 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Tue, 24 Nov 2015 12:10:01 +0000
Subject: [PATCH 03/15] Fix setting the path to the Python package directory.

There were several problems with the existing implementation.

* When specifying ``--prefix`` the implementation would assume the
  path was ``$(PREFIX)/lib/python-<VERSION>/dist-packages``. This
  is incorrect. ``dist-packages`` is Debian (and its derivatives,
  i.e Ubuntu) specific and won't work on other Linux distributions
  such as Arch Linux.

* When generating the ``Makefile``, ``$(PREFIX)`` was only emitted
  during the Python installation when ``--prefix`` was passed on
  the command line. When ``--prefix`` was not passed the absolute
  path to the Python package directory was emitted. This is not
  very consistent.

This patch checks that the detected Python package directory lives
under the install prefix and emits an error if it does not as this
indicates that the installation will be broken. If the Python package
directory does live under the install prefix it replaces that prefix
with the ``$(PREFIX)`` variable when emitting the ``Makefile`` for
consistency with the other install commands.

If a user really wants to install to a particular Python package
directory they can force it with the newly added ``--pypkgdir=``
flag.
---
 scripts/mk_util.py | 32 ++++++++++++++++++++++++++++++--
 1 file changed, 30 insertions(+), 2 deletions(-)

diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 0cad588dc..44779ebb1 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -550,6 +550,7 @@ def display_help(exit_code):
         print("  -p <dir>, --prefix=<dir>      installation prefix (default: %s)." % PREFIX)
     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)
     print("  -b <sudir>, --build=<subdir>  subdirectory where Z3 will be built (default: build).")
     print("  --githash=hash                include the given hash in the binaries.")
     print("  -d, --debug                   compile Z3 in debug mode.")
@@ -593,12 +594,13 @@ 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, JAVA_ENABLED, ML_ENABLED, STATIC_LIB, PREFIX, GMP, FOCI2, FOCI2LIB, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH
     global LINUX_X64, SLOW_OPTIMIZE, USE_OMP
+    pythonPkgDir=None
     try:
         options, remainder = getopt.gnu_getopt(sys.argv[1:],
                                                'b:df:sxhmcvtnp:gj',
                                                ['build=', 'debug', 'silent', 'x64', 'help', 'makefiles', 'showcpp', 'vsproj',
                                                 'trace', 'nodotnet', 'staticlib', 'prefix=', 'gmp', 'foci2=', 'java', 'parallel=', 'gprof',
-                                                'githash=', 'x86', 'ml', 'optimize', 'noomp'])
+                                                'githash=', 'x86', 'ml', 'optimize', 'noomp', 'pypkgdir='])
     except:
         print("ERROR: Invalid command line option")
         display_help(1)
@@ -637,7 +639,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')
+        elif opt in ('--pypkgdir'):
+            pythonPkgDir = arg
         elif IS_WINDOWS and opt == '--parallel':
             VS_PAR = True
             VS_PAR_NUM = int(arg)
@@ -659,6 +662,31 @@ def parse_options():
         else:
             print("ERROR: Invalid command line option '%s'" % opt)
             display_help(1)
+    # Handle the Python package directory
+    def printPythonPackageMessage(errorType):
+        msg = (("%s: The detected Python package directory (%s)"
+               " does not live under the installation prefix (%s)"
+               ". This will most likely lead to a broken installation.") %
+               (errorType, PYTHON_PACKAGE_DIR, PREFIX))
+        if errorType == "ERROR":
+            msg += (" However if you are confident you want to use that"
+                   " Python package directory use --pypkgdir=%s to force"
+                   " it.") % PYTHON_PACKAGE_DIR
+        print(msg)
+    if pythonPkgDir == None:
+        if not IS_WINDOWS:
+            # Try to use the default if it makes sense
+            if not PYTHON_PACKAGE_DIR.startswith(PREFIX):
+                printPythonPackageMessage("ERROR")
+                sys.exit(1)
+            # Do replacement to use $(PREFIX) in the Makefile
+            PYTHON_PACKAGE_DIR = PYTHON_PACKAGE_DIR.replace(PREFIX, "$(PREFIX)", 1)
+    else:
+        PYTHON_PACKAGE_DIR = pythonPkgDir
+        if not os.path.exists(PYTHON_PACKAGE_DIR):
+            print("WARNING: PYTHON_PACKAGE_DIR (%s) does not exist." % PYTHON_PACKAGE_DIR)
+        if not PYTHON_PACKAGE_DIR.startswith(PREFIX):
+            printPythonPackageMessage("WARNING")
 
 # Return a list containing a file names included using '#include' in
 # the given C/C++ file named fname.

From e8822b18065cd162634720c8a9aef7dbde837d99 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Tue, 24 Nov 2015 17:27:54 +0000
Subject: [PATCH 04/15] Add a note about using DESTDIR when building Z3
 completes.

---
 scripts/mk_util.py | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 44779ebb1..f146cd2e5 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -2087,7 +2087,9 @@ def mk_makefile():
     out.write("\t@echo \"Z3Py scripts stored in arbitrary directories can be also executed if \'%s\' directory is added to the PYTHONPATH environment variable.\"\n" % BUILD_DIR)
     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')
+        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')
     # Generate :examples rule
     out.write('examples:')
     for c in get_components():

From 53f0addb6bf86b7a3a03d3ba817019dc3b043cfa Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Tue, 24 Nov 2015 18:15:11 +0000
Subject: [PATCH 05/15] Avoid making a copy of libz3 on non Windows platforms
 for the Python bindings (provided they both exist within the same install
 prefix) by creating a relative symbolic link. This saves space when packaging
 Z3.

---
 scripts/mk_util.py | 50 ++++++++++++++++++++++++++++++++++++++++++++--
 1 file changed, 48 insertions(+), 2 deletions(-)

diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index f146cd2e5..766347b16 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -1246,11 +1246,57 @@ class DLLComponent(Component):
         if self.static:
             out.write(' %s$(LIB_EXT)' % self.dll_name)
 
+    def _compute_relative_path(self, link_dir, target):
+        """
+        Compute the relative path to ``target`` from a directory
+        ``link_dir``.
+
+        e.g.
+        ```
+        self._compute_relative_path("/usr/lib/python3.5/site-packages",
+                                         "/usr/lib/libz3.so")
+
+             ==
+
+             "../../libz3.so"
+        ```
+        """
+        assert os.path.isabs(link_dir)
+        assert os.path.isabs(target)
+        relative_path =""
+
+        temp_path = link_dir
+        # Keep walking up the directory tree until temp_path
+        # is a prefix of target.
+        while not target.startswith(temp_path):
+            assert temp_path != '/'
+            temp_path = os.path.dirname(temp_path)
+            relative_path += '../'
+
+        # Now get the path from the common prefix to the target
+        target_from_prefix = target.replace(temp_path,'',1)
+        relative_path += target_from_prefix
+        # Remove any double slashes
+        relativePath = relative_path.replace('//','/')
+        return relativePath
+
     def mk_install(self, out):
         if self.install:
             dllfile = '%s$(SO_EXT)' % self.dll_name
-            out.write('\t@cp %s %s\n' % (dllfile, os.path.join('$(DESTDIR)$(PREFIX)', 'lib', dllfile)))
-            out.write('\t@cp %s $(DESTDIR)%s\n' % (dllfile, os.path.join(PYTHON_PACKAGE_DIR, dllfile)))
+            dllInstallPath = os.path.join('$(PREFIX)', 'lib', dllfile)
+            pythonPkgDirSubst = PYTHON_PACKAGE_DIR.replace('$(PREFIX)', PREFIX, 1)
+            out.write('\t@cp %s $(DESTDIR)%s\n' % (dllfile, dllInstallPath))
+            if IS_WINDOWS or not pythonPkgDirSubst.startswith(PREFIX):
+                out.write('\t@cp %s $(DESTDIR)%s\n' % (dllfile, os.path.join(PYTHON_PACKAGE_DIR, dllfile)))
+            else:
+                # Create symbolic link to save space.
+                # Compute the relative path from the python package directory
+                # to libz3. It's important that this symlink be relative
+                # (rather than absolute) so that the install is relocatable.
+                dllInstallPathSubst = dllInstallPath.replace('$(PREFIX)', PREFIX,1)
+                relativePath = self._compute_relative_path(pythonPkgDirSubst,
+                                                           dllInstallPathSubst)
+                out.write('\t@ln -s %s $(DESTDIR)%s\n' % (relativePath, os.path.join(PYTHON_PACKAGE_DIR, dllfile)))
             if self.static:
                 libfile = '%s$(LIB_EXT)' % self.dll_name
                 out.write('\t@cp %s %s\n' % (libfile, os.path.join('$(DESTDIR)$(PREFIX)', 'lib', libfile)))

From 23cf7e86a92621af13676cce08c28ade4901b263 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Tue, 24 Nov 2015 23:03:18 +0000
Subject: [PATCH 06/15] Start to address @wintersteiger 's comments aboug
 ``$(DESTDIR)`` being duplicated in too many places and being worried that
 someone might forget to use it when installing additional components.

To acheive this the new ``MakeRuleCmd`` class provides
several class methods to generate commonly needed commands used in
make file rules.

Most of the build system has been changed to use these helper methods
apart from stuff related to the Python bindings. This can't be changed
until we fix how PYTHON_PACKAGE_DIR is handled. Right it not guaranteed
to live under the install prefix but this is a requirement when using
the ``MakeRuleCmd`` methods.
---
 scripts/mk_util.py | 88 +++++++++++++++++++++++++++++++++++++---------
 1 file changed, 72 insertions(+), 16 deletions(-)

diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 766347b16..691633eb2 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -1017,11 +1017,15 @@ class LibComponent(Component):
 
     def mk_install(self, out):
         for include in self.includes2install:
-            out.write('\t@cp %s %s\n' % (os.path.join(self.to_src_dir, include), os.path.join('$(DESTDIR)$(PREFIX)', 'include', include)))
+            MakeRuleCmd.install_files(
+                out,
+                os.path.join(self.to_src_dir, include),
+                os.path.join('include', include)
+            )
 
     def mk_uninstall(self, out):
         for include in self.includes2install:
-            out.write('\t@rm -f %s\n' % os.path.join('$(DESTDIR)$(PREFIX)', 'include', include))
+            MakeRuleCmd.remove_installed_files(out, os.path.join('include', include))
 
     def mk_win_dist(self, build_path, dist_path):
         mk_dir(os.path.join(dist_path, 'include'))
@@ -1103,11 +1107,11 @@ class ExeComponent(Component):
     def mk_install(self, out):
         if self.install:
             exefile = '%s$(EXE_EXT)' % self.exe_name
-            out.write('\t@cp %s %s\n' % (exefile, os.path.join('$(DESTDIR)$(PREFIX)', 'bin', exefile)))
+            MakeRuleCmd.install_files(out, exefile, os.path.join('bin', exefile))
 
     def mk_uninstall(self, out):
         exefile = '%s$(EXE_EXT)' % self.exe_name
-        out.write('\t@rm -f %s\n' % os.path.join('$(DESTDIR)$(PREFIX)', 'bin', exefile))
+        MakeRuleCmd.remove_installed_files(out, os.path.join('bin', exefile))
 
     def mk_win_dist(self, build_path, dist_path):
         if self.install:
@@ -1283,9 +1287,11 @@ class DLLComponent(Component):
     def mk_install(self, out):
         if self.install:
             dllfile = '%s$(SO_EXT)' % self.dll_name
+            MakeRuleCmd.install_files(out, dllfile, os.path.join('lib', dllfile))
+            # FIXME: All this stuff to do with the Python bindings needs to
+            # be refactored to use MakeRuleCmd.
             dllInstallPath = os.path.join('$(PREFIX)', 'lib', dllfile)
             pythonPkgDirSubst = PYTHON_PACKAGE_DIR.replace('$(PREFIX)', PREFIX, 1)
-            out.write('\t@cp %s $(DESTDIR)%s\n' % (dllfile, dllInstallPath))
             if IS_WINDOWS or not pythonPkgDirSubst.startswith(PREFIX):
                 out.write('\t@cp %s $(DESTDIR)%s\n' % (dllfile, os.path.join(PYTHON_PACKAGE_DIR, dllfile)))
             else:
@@ -1299,15 +1305,15 @@ class DLLComponent(Component):
                 out.write('\t@ln -s %s $(DESTDIR)%s\n' % (relativePath, os.path.join(PYTHON_PACKAGE_DIR, dllfile)))
             if self.static:
                 libfile = '%s$(LIB_EXT)' % self.dll_name
-                out.write('\t@cp %s %s\n' % (libfile, os.path.join('$(DESTDIR)$(PREFIX)', 'lib', libfile)))
-
+                MakeRuleCmd.install_files(out, libfile, os.path.join('lib', libfile))
 
     def mk_uninstall(self, out):
         dllfile = '%s$(SO_EXT)' % self.dll_name
-        out.write('\t@rm -f %s\n' % os.path.join('$(DESTDIR)$(PREFIX)', 'lib', dllfile))
+        MakeRuleCmd.remove_installed_files(out, os.path.join('lib', dllfile))
+        # FIXME: Use MakeRuleCmd
         out.write('\t@rm -f $(DESTDIR)%s\n' % os.path.join(PYTHON_PACKAGE_DIR, dllfile))
         libfile = '%s$(LIB_EXT)' % self.dll_name
-        out.write('\t@rm -f %s\n' % os.path.join('$(DESTDIR)$(PREFIX)', 'lib', libfile))
+        MakeRuleCmd.remove_installed_files(out, os.path.join('lib', libfile))
 
     def mk_win_dist(self, build_path, dist_path):
         if self.install:
@@ -1474,14 +1480,16 @@ class JavaDLLComponent(Component):
     def mk_install(self, out):
         if is_java_enabled() and self.install:
             dllfile = '%s$(SO_EXT)' % self.dll_name
-            out.write('\t@cp %s %s\n' % (dllfile, os.path.join('$(PREFIX)', 'lib', dllfile)))
-            out.write('\t@cp %s.jar %s.jar\n' % (self.package_name, os.path.join('$(PREFIX)', 'lib', self.package_name)))
+            MakeRuleCmd.install_files(out, dllfile, os.path.join('lib', dllfile))
+            jarfile = '{}.jar'.format(self.package_name)
+            MakeRuleCmd.install_files(out, jarfile, os.path.join('lib', jarfile))
 
     def mk_uninstall(self, out):
         if is_java_enabled() and self.install:
             dllfile = '%s$(SO_EXT)' % self.dll_name
-            out.write('\t@rm %s\n' % (os.path.join('$(PREFIX)', 'lib', dllfile)))
-            out.write('\t@rm %s.jar\n' % (os.path.join('$(PREFIX)', 'lib', self.package_name)))
+            MakeRuleCmd.remove_installed_files(out, os.path.join('lib', dllfile))
+            jarfile = '{}.jar'.format(self.package_name)
+            MakeRuleCmd.remove_installed_files(out, os.path.join('lib', jarfile))
 
 class MLComponent(Component):
     def __init__(self, name, lib_name, path, deps):
@@ -2080,9 +2088,10 @@ def mk_install(out):
     if is_ml_enabled() and OCAMLFIND != '':
         out.write('ocamlfind_install')
     out.write('\n')
-    out.write('\t@mkdir -p %s\n' % os.path.join('$(DESTDIR)$(PREFIX)', 'bin'))
-    out.write('\t@mkdir -p %s\n' % os.path.join('$(DESTDIR)$(PREFIX)', 'include'))
-    out.write('\t@mkdir -p %s\n' % os.path.join('$(DESTDIR)$(PREFIX)', 'lib'))
+    MakeRuleCmd.make_install_directory(out, 'bin')
+    MakeRuleCmd.make_install_directory(out, 'include')
+    MakeRuleCmd.make_install_directory(out, 'lib')
+    # FIXME: use MakeRuleCmd for the Python stuff
     out.write('\t@mkdir -p $(DESTDIR)%s\n' % PYTHON_PACKAGE_DIR)
     for c in get_components():
         c.mk_install(out)
@@ -2108,6 +2117,7 @@ def mk_uninstall(out):
     out.write('uninstall:\n')
     for c in get_components():
         c.mk_uninstall(out)
+    # FIXME: use MakeRuleCmd for the Python stuff
     out.write('\t@rm -f $(DESTDIR)%s*.py\n' % os.path.join(PYTHON_PACKAGE_DIR, 'z3'))
     out.write('\t@rm -f $(DESTDIR)%s*.pyc\n' % os.path.join(PYTHON_PACKAGE_DIR, 'z3'))
     out.write('\t@rm -f $(DESTDIR)%s*.pyc\n' % os.path.join(PYTHON_PACKAGE_DIR, '__pycache__', 'z3'))
@@ -3260,6 +3270,52 @@ def mk_unix_dist(build_path, dist_path):
         shutil.copy(os.path.join(build_path, pyc),
                     os.path.join(dist_path, 'bin', pyc))
 
+class MakeRuleCmd(object):
+    """
+        These class methods provide a convenient way to emit frequently
+        needed commands used in Makefile rules
+
+        Note that several of the method are meant for use during ``make
+        install`` and ``make uninstall``.  These methods correctly use
+        ``$(PREFIX)`` and ``$(DESTDIR)`` and therefore are preferrable
+        to writing commands manually which can be error prone.
+    """
+    @classmethod
+    def install_files(cls, out, srcPattern, dest):
+        assert len(dest) > 0
+        assert isinstance(srcPattern, str)
+        assert not ' ' in srcPattern
+        assert isinstance(dest, str)
+        assert not ' ' in dest
+        assert not os.path.isabs(srcPattern)
+        assert not os.path.isabs(dest)
+        cls.write_cmd(out, "cp {} $(DESTDIR)$(PREFIX)/{}".format(srcPattern, dest))
+
+    @classmethod
+    def remove_installed_files(cls, out, pattern):
+        assert len(pattern) > 0
+        assert isinstance(pattern, str)
+        assert not ' ' in pattern
+        assert not os.path.isabs(pattern)
+        cls.write_cmd(out, "rm -f $(DESTDIR)$(PREFIX)/{}".format(pattern))
+
+    @classmethod
+    def make_install_directory(cls, out, dir):
+        assert len(dir) > 0
+        assert isinstance(dir, str)
+        assert not ' ' in dir
+        assert not os.path.isabs(dir)
+        cls.write_cmd(out, "mkdir -p $(DESTDIR)$(PREFIX)/{}".format(dir))
+
+    # TODO: Refactor all of the build system to emit commands using this
+    # helper to simplify code. This will also let us replace ``@`` with
+    # ``$(Verb)`` and have it set to ``@`` or empty at build time depending on
+    # a variable (e.g. ``VERBOSE``) passed to the ``make`` invocation. This
+    # would be very helpful for debugging.
+    @classmethod
+    def write_cmd(cls, out, line):
+        out.write("\t@{}\n".format(line))
+
 
 if __name__ == '__main__':
     import doctest

From 041c02feb7aa682ecc887a2a1064b5729c68a5b4 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Wed, 25 Nov 2015 10:46:56 +0000
Subject: [PATCH 07/15] Finish addressing @wintersteiger comments on
 ``$(DESTDIR)`` being duplicated in too many places by refactoring the
 installation and removal of the Python bindings to use the ``MakeRuleCmd``
 class.

In order to make this change:

* ``PYTHON_PACKAGE_DIR`` no longer contains the text ``$(PREFIX)``
* ``PYTHON_PACKAGE_DIR`` **MUST BE** inside the installation prefix
---
 scripts/mk_util.py | 166 ++++++++++++++++++++++-----------------------
 1 file changed, 83 insertions(+), 83 deletions(-)

diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 691633eb2..7bc68e193 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -594,7 +594,6 @@ 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, JAVA_ENABLED, ML_ENABLED, STATIC_LIB, PREFIX, GMP, FOCI2, FOCI2LIB, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH
     global LINUX_X64, SLOW_OPTIMIZE, USE_OMP
-    pythonPkgDir=None
     try:
         options, remainder = getopt.gnu_getopt(sys.argv[1:],
                                                'b:df:sxhmcvtnp:gj',
@@ -640,7 +639,7 @@ def parse_options():
         elif not IS_WINDOWS and opt in ('-p', '--prefix'):
             PREFIX = arg
         elif opt in ('--pypkgdir'):
-            pythonPkgDir = arg
+            PYTHON_PACKAGE_DIR = arg
         elif IS_WINDOWS and opt == '--parallel':
             VS_PAR = True
             VS_PAR_NUM = int(arg)
@@ -663,30 +662,15 @@ def parse_options():
             print("ERROR: Invalid command line option '%s'" % opt)
             display_help(1)
     # Handle the Python package directory
-    def printPythonPackageMessage(errorType):
-        msg = (("%s: The detected Python package directory (%s)"
-               " does not live under the installation prefix (%s)"
-               ". This will most likely lead to a broken installation.") %
-               (errorType, PYTHON_PACKAGE_DIR, PREFIX))
-        if errorType == "ERROR":
-            msg += (" However if you are confident you want to use that"
-                   " Python package directory use --pypkgdir=%s to force"
-                   " it.") % PYTHON_PACKAGE_DIR
-        print(msg)
-    if pythonPkgDir == None:
-        if not IS_WINDOWS:
-            # Try to use the default if it makes sense
-            if not PYTHON_PACKAGE_DIR.startswith(PREFIX):
-                printPythonPackageMessage("ERROR")
-                sys.exit(1)
-            # Do replacement to use $(PREFIX) in the Makefile
-            PYTHON_PACKAGE_DIR = PYTHON_PACKAGE_DIR.replace(PREFIX, "$(PREFIX)", 1)
-    else:
-        PYTHON_PACKAGE_DIR = pythonPkgDir
-        if not os.path.exists(PYTHON_PACKAGE_DIR):
-            print("WARNING: PYTHON_PACKAGE_DIR (%s) does not exist." % PYTHON_PACKAGE_DIR)
+    if not IS_WINDOWS:
         if not PYTHON_PACKAGE_DIR.startswith(PREFIX):
-            printPythonPackageMessage("WARNING")
+            printPythonPackageMessage("ERROR")
+            print(("ERROR: The detected Python package directory (%s)"
+                   " does not live under the installation prefix (%s)"
+                   ". This would lead to a broken installation."
+                   "Use --pypkgdir= to change the Python package directory") %
+                  (errorType, PYTHON_PACKAGE_DIR, PREFIX))
+            sys.exit(1)
 
 # Return a list containing a file names included using '#include' in
 # the given C/C++ file named fname.
@@ -1250,59 +1234,21 @@ class DLLComponent(Component):
         if self.static:
             out.write(' %s$(LIB_EXT)' % self.dll_name)
 
-    def _compute_relative_path(self, link_dir, target):
-        """
-        Compute the relative path to ``target`` from a directory
-        ``link_dir``.
-
-        e.g.
-        ```
-        self._compute_relative_path("/usr/lib/python3.5/site-packages",
-                                         "/usr/lib/libz3.so")
-
-             ==
-
-             "../../libz3.so"
-        ```
-        """
-        assert os.path.isabs(link_dir)
-        assert os.path.isabs(target)
-        relative_path =""
-
-        temp_path = link_dir
-        # Keep walking up the directory tree until temp_path
-        # is a prefix of target.
-        while not target.startswith(temp_path):
-            assert temp_path != '/'
-            temp_path = os.path.dirname(temp_path)
-            relative_path += '../'
-
-        # Now get the path from the common prefix to the target
-        target_from_prefix = target.replace(temp_path,'',1)
-        relative_path += target_from_prefix
-        # Remove any double slashes
-        relativePath = relative_path.replace('//','/')
-        return relativePath
-
     def mk_install(self, out):
         if self.install:
             dllfile = '%s$(SO_EXT)' % self.dll_name
-            MakeRuleCmd.install_files(out, dllfile, os.path.join('lib', dllfile))
-            # FIXME: All this stuff to do with the Python bindings needs to
-            # be refactored to use MakeRuleCmd.
-            dllInstallPath = os.path.join('$(PREFIX)', 'lib', dllfile)
-            pythonPkgDirSubst = PYTHON_PACKAGE_DIR.replace('$(PREFIX)', PREFIX, 1)
-            if IS_WINDOWS or not pythonPkgDirSubst.startswith(PREFIX):
-                out.write('\t@cp %s $(DESTDIR)%s\n' % (dllfile, os.path.join(PYTHON_PACKAGE_DIR, dllfile)))
+            dllInstallPath = os.path.join('lib', dllfile)
+            MakeRuleCmd.install_files(out, dllfile, dllInstallPath)
+            pythonPkgDirWithoutPrefix = strip_path_prefix(PYTHON_PACKAGE_DIR, PREFIX)
+            if IS_WINDOWS:
+                MakeRuleCmd.install_files(dllfile, os.path.join(pythonPkgDirWithoutPrefix, dllfile))
             else:
                 # Create symbolic link to save space.
                 # Compute the relative path from the python package directory
                 # to libz3. It's important that this symlink be relative
                 # (rather than absolute) so that the install is relocatable.
-                dllInstallPathSubst = dllInstallPath.replace('$(PREFIX)', PREFIX,1)
-                relativePath = self._compute_relative_path(pythonPkgDirSubst,
-                                                           dllInstallPathSubst)
-                out.write('\t@ln -s %s $(DESTDIR)%s\n' % (relativePath, os.path.join(PYTHON_PACKAGE_DIR, dllfile)))
+                dllInstallPathAbs = os.path.join(PREFIX, dllInstallPath)
+                MakeRuleCmd.create_relative_symbolic_link(out, dllInstallPath, os.path.join(pythonPkgDirWithoutPrefix, dllfile))
             if self.static:
                 libfile = '%s$(LIB_EXT)' % self.dll_name
                 MakeRuleCmd.install_files(out, libfile, os.path.join('lib', libfile))
@@ -1310,8 +1256,8 @@ class DLLComponent(Component):
     def mk_uninstall(self, out):
         dllfile = '%s$(SO_EXT)' % self.dll_name
         MakeRuleCmd.remove_installed_files(out, os.path.join('lib', dllfile))
-        # FIXME: Use MakeRuleCmd
-        out.write('\t@rm -f $(DESTDIR)%s\n' % os.path.join(PYTHON_PACKAGE_DIR, dllfile))
+        pythonPkgDirWithoutPrefix = strip_path_prefix(PYTHON_PACKAGE_DIR, PREFIX)
+        MakeRuleCmd.remove_installed_files(out, os.path.join(pythonPkgDirWithoutPrefix, dllfile))
         libfile = '%s$(LIB_EXT)' % self.dll_name
         MakeRuleCmd.remove_installed_files(out, os.path.join('lib', libfile))
 
@@ -2091,17 +2037,17 @@ def mk_install(out):
     MakeRuleCmd.make_install_directory(out, 'bin')
     MakeRuleCmd.make_install_directory(out, 'include')
     MakeRuleCmd.make_install_directory(out, 'lib')
-    # FIXME: use MakeRuleCmd for the Python stuff
-    out.write('\t@mkdir -p $(DESTDIR)%s\n' % PYTHON_PACKAGE_DIR)
+    pythonPkgDirWithoutPrefix = strip_path_prefix(PYTHON_PACKAGE_DIR, PREFIX)
+    MakeRuleCmd.make_install_directory(out, pythonPkgDirWithoutPrefix)
     for c in get_components():
         c.mk_install(out)
-    out.write('\t@cp z3*.py $(DESTDIR)%s\n' % PYTHON_PACKAGE_DIR)
+    MakeRuleCmd.install_files(out, 'z3*.py', pythonPkgDirWithoutPrefix)
     if sys.version >= "3":
-        out.write('\t@mkdir -p $(DESTDIR)%s\n' % os.path.join(PYTHON_PACKAGE_DIR, '__pycache__'))
-        out.write('\t@cp %s*.pyc $(DESTDIR)%s\n' % (os.path.join('__pycache__', 'z3'),
-                                          os.path.join(PYTHON_PACKAGE_DIR, '__pycache__')))
+        pythonPycacheDir = os.path.join(pythonPkgDirWithoutPrefix, '__pycache__')
+        MakeRuleCmd.make_install_directory(out, pythonPycacheDir)
+        MakeRuleCmd.install_files(out, '{}*.pyc'.format(os.path.join('__pycache__', 'z3')), pythonPycacheDir)
     else:
-        out.write('\t@cp z3*.pyc $(DESTDIR)%s\n' % PYTHON_PACKAGE_DIR)
+        MakeRuleCmd.install_files(out, 'z3*.pyc', pythonPkgDirWithoutPrefix)
     out.write('\t@echo Z3 was successfully installed.\n')
     if PYTHON_PACKAGE_DIR != distutils.sysconfig.get_python_lib():
         if os.uname()[0] == 'Darwin':
@@ -2117,10 +2063,10 @@ def mk_uninstall(out):
     out.write('uninstall:\n')
     for c in get_components():
         c.mk_uninstall(out)
-    # FIXME: use MakeRuleCmd for the Python stuff
-    out.write('\t@rm -f $(DESTDIR)%s*.py\n' % os.path.join(PYTHON_PACKAGE_DIR, 'z3'))
-    out.write('\t@rm -f $(DESTDIR)%s*.pyc\n' % os.path.join(PYTHON_PACKAGE_DIR, 'z3'))
-    out.write('\t@rm -f $(DESTDIR)%s*.pyc\n' % os.path.join(PYTHON_PACKAGE_DIR, '__pycache__', 'z3'))
+    pythonPkgDirWithoutPrefix = strip_path_prefix(PYTHON_PACKAGE_DIR, PREFIX)
+    MakeRuleCmd.remove_installed_files(out, '{}*.py'.format(os.path.join(pythonPkgDirWithoutPrefix, 'z3')))
+    MakeRuleCmd.remove_installed_files(out, '{}*.pyc'.format(os.path.join(pythonPkgDirWithoutPrefix, 'z3')))
+    MakeRuleCmd.remove_installed_files(out, '{}*.pyc'.format(os.path.join(pythonPkgDirWithoutPrefix, '__pycache__', 'z3')))
     out.write('\t@echo Z3 was successfully uninstalled.\n')
     out.write('\n')
 
@@ -3307,6 +3253,51 @@ class MakeRuleCmd(object):
         assert not os.path.isabs(dir)
         cls.write_cmd(out, "mkdir -p $(DESTDIR)$(PREFIX)/{}".format(dir))
 
+    @classmethod
+    def create_relative_symbolic_link(cls, out, target, link_name):
+        assert isinstance(target, str)
+        assert isinstance(link_name, str)
+        assert len(target) > 0
+        assert len(link_name) > 0
+        assert not os.path.isabs(target)
+        assert not os.path.isabs(link_name)
+
+        # We can't test to see if link_name is a file or directory
+        # because it may not exist yet. Instead follow the convention
+        # that if there is a leading slash target is a directory otherwise
+        # it's a file
+        if link_name[-1] != '/':
+            # link_name is a file
+            temp_path = '/' + os.path.dirname(link_name)
+        else:
+            # link_name is a directory
+            temp_path = '/' + link_name[:-1]
+        relative_path = ""
+        targetAsAbs = '/' + target
+        assert os.path.isabs(targetAsAbs)
+        assert os.path.isabs(temp_path)
+        # Keep walking up the directory tree until temp_path
+        # is a prefix of targetAsAbs
+        while not targetAsAbs.startswith(temp_path):
+            assert temp_path != '/'
+            temp_path = os.path.dirname(temp_path)
+            relative_path += '../'
+
+        # Now get the path from the common prefix directory to the target
+        target_from_prefix = targetAsAbs[len(temp_path):]
+        relative_path += target_from_prefix
+        # Remove any double slashes
+        relative_path = relative_path.replace('//','/')
+        cls.create_symbolic_link(out, relative_path, link_name)
+
+    @classmethod
+    def create_symbolic_link(cls, out, target, link_name):
+        assert isinstance(target, str)
+        assert isinstance(link_name, str)
+        assert not os.path.isabs(target)
+        assert not os.path.isabs(link_name)
+        cls.write_cmd(out, 'ln -s {} $(DESTDIR)$(PREFIX)/{}'.format(target, link_name))
+
     # TODO: Refactor all of the build system to emit commands using this
     # helper to simplify code. This will also let us replace ``@`` with
     # ``$(Verb)`` and have it set to ``@`` or empty at build time depending on
@@ -3316,6 +3307,15 @@ class MakeRuleCmd(object):
     def write_cmd(cls, out, line):
         out.write("\t@{}\n".format(line))
 
+def strip_path_prefix(path, prefix):
+    assert path.startswith(prefix)
+    stripped_path = path[len(prefix):]
+    stripped_path.replace('//','/')
+    if stripped_path[0] == '/':
+        stripped_path = stripped_path[1:]
+
+    assert not os.path.isabs(stripped_path)
+    return stripped_path
 
 if __name__ == '__main__':
     import doctest

From d6fa0583abee1a1030a3faef0169cebbbebafced Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Wed, 25 Nov 2015 11:02:59 +0000
Subject: [PATCH 08/15] Fix bug in ``ExeComponent.mk_uninstall()`` in the build
 system which would try to uninstall components that were never installed.

This bug would cause the following line to be emitted in the
``Makefile`` under the ``uninstall`` rule even though there was
no corresponding rule to install the file under the ``install`` rule.

```
@rm -f $(DESTDIR)$(PREFIX)/bin/test-z3$(EXE_EXT)
```
---
 scripts/mk_util.py | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 7bc68e193..8b75761fe 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -1094,8 +1094,9 @@ class ExeComponent(Component):
             MakeRuleCmd.install_files(out, exefile, os.path.join('bin', exefile))
 
     def mk_uninstall(self, out):
-        exefile = '%s$(EXE_EXT)' % self.exe_name
-        MakeRuleCmd.remove_installed_files(out, os.path.join('bin', exefile))
+        if self.install:
+            exefile = '%s$(EXE_EXT)' % self.exe_name
+            MakeRuleCmd.remove_installed_files(out, os.path.join('bin', exefile))
 
     def mk_win_dist(self, build_path, dist_path):
         if self.install:

From 6984070b3a742e9bccd65f9e2e2d447c3eecfe84 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Wed, 25 Nov 2015 11:28:51 +0000
Subject: [PATCH 09/15] Fix typo (missing argument) that I missed that didn't
 fire because I did not test on Windows.

---
 scripts/mk_util.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 8b75761fe..5563c29a3 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -1242,7 +1242,7 @@ class DLLComponent(Component):
             MakeRuleCmd.install_files(out, dllfile, dllInstallPath)
             pythonPkgDirWithoutPrefix = strip_path_prefix(PYTHON_PACKAGE_DIR, PREFIX)
             if IS_WINDOWS:
-                MakeRuleCmd.install_files(dllfile, os.path.join(pythonPkgDirWithoutPrefix, dllfile))
+                MakeRuleCmd.install_files(out, dllfile, os.path.join(pythonPkgDirWithoutPrefix, dllfile))
             else:
                 # Create symbolic link to save space.
                 # Compute the relative path from the python package directory

From 684318149b2112b0644473cb96f64024aedf8957 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Wed, 25 Nov 2015 11:31:49 +0000
Subject: [PATCH 10/15] Remove dead code that I accidently left behind.

---
 scripts/mk_util.py | 1 -
 1 file changed, 1 deletion(-)

diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 5563c29a3..cd1dd9bd1 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -1248,7 +1248,6 @@ class DLLComponent(Component):
                 # Compute the relative path from the python package directory
                 # to libz3. It's important that this symlink be relative
                 # (rather than absolute) so that the install is relocatable.
-                dllInstallPathAbs = os.path.join(PREFIX, dllInstallPath)
                 MakeRuleCmd.create_relative_symbolic_link(out, dllInstallPath, os.path.join(pythonPkgDirWithoutPrefix, dllfile))
             if self.static:
                 libfile = '%s$(LIB_EXT)' % self.dll_name

From 32c4384d4834c56f532386d2b133a92b57acd072 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Wed, 25 Nov 2015 16:00:35 +0000
Subject: [PATCH 11/15] Fix dead comment and expand on the reasons for making a
 symbolic link slightly.

---
 scripts/mk_util.py | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index cd1dd9bd1..fd8c713d4 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -1245,9 +1245,9 @@ class DLLComponent(Component):
                 MakeRuleCmd.install_files(out, dllfile, os.path.join(pythonPkgDirWithoutPrefix, dllfile))
             else:
                 # Create symbolic link to save space.
-                # Compute the relative path from the python package directory
-                # to libz3. It's important that this symlink be relative
-                # (rather than absolute) so that the install is relocatable.
+                # It's important that this symbolic link be relative (rather
+                # than absolute) so that the install is relocatable (needed for
+                # staged installs that use DESTDIR).
                 MakeRuleCmd.create_relative_symbolic_link(out, dllInstallPath, os.path.join(pythonPkgDirWithoutPrefix, dllfile))
             if self.static:
                 libfile = '%s$(LIB_EXT)' % self.dll_name

From f1d4f36ddf3c1ec51cc5949a130231b77ba75648 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Wed, 25 Nov 2015 18:50:02 +0000
Subject: [PATCH 12/15] Refactor the use of ``$(DESTDIR)$(PREFIX)`` in
 ``MakeRuleCmd`` class so that it is exposed via a public method
 (``install_root()``) so that is can be used externally. Also refactor the
 existing methods to use it.

---
 scripts/mk_util.py | 35 +++++++++++++++++++++++++++--------
 1 file changed, 27 insertions(+), 8 deletions(-)

diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index fd8c713d4..c6aedf6ff 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -3227,15 +3227,27 @@ class MakeRuleCmd(object):
         to writing commands manually which can be error prone.
     """
     @classmethod
-    def install_files(cls, out, srcPattern, dest):
+    def install_root(cls):
+        """
+            Returns a string that will expand to the
+            install location when used in a makefile rule.
+        """
+        # Note: DESTDIR is to support staged installs
+        return "$(DESTDIR)$(PREFIX)/"
+
+    @classmethod
+    def install_files(cls, out, src_pattern, dest):
         assert len(dest) > 0
-        assert isinstance(srcPattern, str)
-        assert not ' ' in srcPattern
+        assert isinstance(src_pattern, str)
+        assert not ' ' in src_pattern
         assert isinstance(dest, str)
         assert not ' ' in dest
-        assert not os.path.isabs(srcPattern)
+        assert not os.path.isabs(src_pattern)
         assert not os.path.isabs(dest)
-        cls.write_cmd(out, "cp {} $(DESTDIR)$(PREFIX)/{}".format(srcPattern, dest))
+        cls.write_cmd(out, "cp {src_pattern} {install_root}{dest}".format(
+            src_pattern=src_pattern,
+            install_root=cls.install_root(),
+            dest=dest))
 
     @classmethod
     def remove_installed_files(cls, out, pattern):
@@ -3243,7 +3255,9 @@ class MakeRuleCmd(object):
         assert isinstance(pattern, str)
         assert not ' ' in pattern
         assert not os.path.isabs(pattern)
-        cls.write_cmd(out, "rm -f $(DESTDIR)$(PREFIX)/{}".format(pattern))
+        cls.write_cmd(out, "rm -f {install_root}{pattern}".format(
+            install_root=cls.install_root(),
+            pattern=pattern))
 
     @classmethod
     def make_install_directory(cls, out, dir):
@@ -3251,7 +3265,9 @@ class MakeRuleCmd(object):
         assert isinstance(dir, str)
         assert not ' ' in dir
         assert not os.path.isabs(dir)
-        cls.write_cmd(out, "mkdir -p $(DESTDIR)$(PREFIX)/{}".format(dir))
+        cls.write_cmd(out, "mkdir -p {install_root}{dir}".format(
+            install_root=cls.install_root(),
+            dir=dir))
 
     @classmethod
     def create_relative_symbolic_link(cls, out, target, link_name):
@@ -3296,7 +3312,10 @@ class MakeRuleCmd(object):
         assert isinstance(link_name, str)
         assert not os.path.isabs(target)
         assert not os.path.isabs(link_name)
-        cls.write_cmd(out, 'ln -s {} $(DESTDIR)$(PREFIX)/{}'.format(target, link_name))
+        cls.write_cmd(out, 'ln -s {target} {install_root}{link_name}'.format(
+            target=target,
+            install_root=cls.install_root(),
+            link_name=link_name))
 
     # TODO: Refactor all of the build system to emit commands using this
     # helper to simplify code. This will also let us replace ``@`` with

From d205b176e8bb725b6e14ef2482fd5873c378ed86 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Sat, 28 Nov 2015 18:53:42 +0000
Subject: [PATCH 13/15] Bug fix for
 ``MakeRuleCmd.create_relative_symbolic_link()``.

create_relative_symbolic_link(out, '/usr/lib64/libz3.so',
'/usr/lib/python3.5/site-package/libz3.so') would create an incorrect relative
path because it would consider ``/usr/lib`` to a be a path prefix of
``/usr/lib64``.
---
 scripts/mk_util.py | 23 ++++++++++++++++++++++-
 1 file changed, 22 insertions(+), 1 deletion(-)

diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index c6aedf6ff..e166e8010 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -3269,6 +3269,27 @@ class MakeRuleCmd(object):
             install_root=cls.install_root(),
             dir=dir))
 
+    @classmethod
+    def _is_path_prefix_of(cls, temp_path, target_as_abs):
+        """
+            Returns True iff ``temp_path`` is a path prefix
+            of ``target_as_abs``
+        """
+        assert isinstance(temp_path, str)
+        assert isinstance(target_as_abs, str)
+        assert len(temp_path) > 0
+        assert len(target_as_abs) > 0
+        assert os.path.isabs(temp_path)
+        assert os.path.isabs(target_as_abs)
+
+        # Need to stick extra slash in front otherwise we might think that
+        # ``/lib`` is a prefix of ``/lib64``.  Of course if ``temp_path ==
+        # '/'`` then we shouldn't else we would check if ``//`` (rather than
+        # ``/``) is a prefix of ``/lib64``, which would fail.
+        if len(temp_path) > 1:
+            temp_path += os.sep
+        return target_as_abs.startswith(temp_path)
+
     @classmethod
     def create_relative_symbolic_link(cls, out, target, link_name):
         assert isinstance(target, str)
@@ -3294,7 +3315,7 @@ class MakeRuleCmd(object):
         assert os.path.isabs(temp_path)
         # Keep walking up the directory tree until temp_path
         # is a prefix of targetAsAbs
-        while not targetAsAbs.startswith(temp_path):
+        while not cls._is_path_prefix_of(temp_path, targetAsAbs):
             assert temp_path != '/'
             temp_path = os.path.dirname(temp_path)
             relative_path += '../'

From d2ba6f0ebfc4d4d5713926f00604ec39424463bb Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Sat, 28 Nov 2015 17:48:49 +0000
Subject: [PATCH 14/15] Provide a way to customise the install directories via
 environment variables:

Z3_INSTALL_BIN_DIR - defaults to "bin"
Z3_INSTALL_LIB_DIR - defaults to "lib"
Z3_INSTALL_INCLUDE_DIR - defaults to "include"

This has two advantages

* We no longer hard code strings like "bin" all over the place
* Packagers can easily control where things get installed.
---
 scripts/mk_util.py | 89 +++++++++++++++++++++++++---------------------
 1 file changed, 48 insertions(+), 41 deletions(-)

diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index e166e8010..d7021b570 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -34,6 +34,10 @@ OCAMLC=getenv("OCAMLC", "ocamlc")
 OCAMLOPT=getenv("OCAMLOPT", "ocamlopt")
 OCAML_LIB=getenv("OCAML_LIB", None)
 OCAMLFIND=getenv("OCAMLFIND", "ocamlfind")
+# Standard install directories relative to PREFIX
+INSTALL_BIN_DIR=getenv("Z3_INSTALL_BIN_DIR", "bin")
+INSTALL_LIB_DIR=getenv("Z3_INSTALL_LIB_DIR", "lib")
+INSTALL_INCLUDE_DIR=getenv("Z3_INSTALL_INCLUDE_DIR", "include")
 
 CXX_COMPILERS=['g++', 'clang++']
 C_COMPILERS=['gcc', 'clang']
@@ -587,6 +591,9 @@ def display_help(exit_code):
     print("  OCAMLC     Ocaml byte-code compiler (only relevant with --ml)")
     print("  OCAMLOPT   Ocaml native compiler (only relevant with --ml)")
     print("  OCAML_LIB  Ocaml library directory (only relevant with --ml)")
+    print("  Z3_INSTALL_BIN_DIR Install directory for binaries relative to install prefix")
+    print("  Z3_INSTALL_LIB_DIR Install directory for libraries relative to install prefix")
+    print("  Z3_INSTALL_INCLUDE_DIR Install directory for header files relative to install prefix")
     exit(exit_code)
 
 # Parse configuration option for mk_make script
@@ -1004,18 +1011,18 @@ class LibComponent(Component):
             MakeRuleCmd.install_files(
                 out,
                 os.path.join(self.to_src_dir, include),
-                os.path.join('include', include)
+                os.path.join(INSTALL_INCLUDE_DIR, include)
             )
 
     def mk_uninstall(self, out):
         for include in self.includes2install:
-            MakeRuleCmd.remove_installed_files(out, os.path.join('include', include))
+            MakeRuleCmd.remove_installed_files(out, os.path.join(INSTALL_INCLUDE_DIR, include))
 
     def mk_win_dist(self, build_path, dist_path):
-        mk_dir(os.path.join(dist_path, 'include'))
+        mk_dir(os.path.join(dist_path, INSTALL_INCLUDE_DIR))
         for include in self.includes2install:
             shutil.copy(os.path.join(self.src_dir, include),
-                        os.path.join(dist_path, 'include', include))
+                        os.path.join(dist_path, INSTALL_INCLUDE_DIR, include))
 
     def mk_unix_dist(self, build_path, dist_path):
         self.mk_win_dist(build_path, dist_path)
@@ -1091,24 +1098,24 @@ class ExeComponent(Component):
     def mk_install(self, out):
         if self.install:
             exefile = '%s$(EXE_EXT)' % self.exe_name
-            MakeRuleCmd.install_files(out, exefile, os.path.join('bin', exefile))
+            MakeRuleCmd.install_files(out, exefile, os.path.join(INSTALL_BIN_DIR, exefile))
 
     def mk_uninstall(self, out):
         if self.install:
             exefile = '%s$(EXE_EXT)' % self.exe_name
-            MakeRuleCmd.remove_installed_files(out, os.path.join('bin', exefile))
+            MakeRuleCmd.remove_installed_files(out, os.path.join(INSTALL_BIN_DIR, exefile))
 
     def mk_win_dist(self, build_path, dist_path):
         if self.install:
-            mk_dir(os.path.join(dist_path, 'bin'))
+            mk_dir(os.path.join(dist_path, INSTALL_BIN_DIR))
             shutil.copy('%s.exe' % os.path.join(build_path, self.exe_name),
-                        '%s.exe' % os.path.join(dist_path, 'bin', self.exe_name))
+                        '%s.exe' % os.path.join(dist_path, INSTALL_BIN_DIR, self.exe_name))
 
     def mk_unix_dist(self, build_path, dist_path):
         if self.install:
-            mk_dir(os.path.join(dist_path, 'bin'))
+            mk_dir(os.path.join(dist_path, INSTALL_BIN_DIR))
             shutil.copy(os.path.join(build_path, self.exe_name),
-                        os.path.join(dist_path, 'bin', self.exe_name))
+                        os.path.join(dist_path, INSTALL_BIN_DIR, self.exe_name))
 
 
 class ExtraExeComponent(ExeComponent):
@@ -1238,7 +1245,7 @@ class DLLComponent(Component):
     def mk_install(self, out):
         if self.install:
             dllfile = '%s$(SO_EXT)' % self.dll_name
-            dllInstallPath = os.path.join('lib', dllfile)
+            dllInstallPath = os.path.join(INSTALL_LIB_DIR, dllfile)
             MakeRuleCmd.install_files(out, dllfile, dllInstallPath)
             pythonPkgDirWithoutPrefix = strip_path_prefix(PYTHON_PACKAGE_DIR, PREFIX)
             if IS_WINDOWS:
@@ -1251,32 +1258,32 @@ class DLLComponent(Component):
                 MakeRuleCmd.create_relative_symbolic_link(out, dllInstallPath, os.path.join(pythonPkgDirWithoutPrefix, dllfile))
             if self.static:
                 libfile = '%s$(LIB_EXT)' % self.dll_name
-                MakeRuleCmd.install_files(out, libfile, os.path.join('lib', libfile))
+                MakeRuleCmd.install_files(out, libfile, os.path.join(INSTALL_LIB_DIR, libfile))
 
     def mk_uninstall(self, out):
         dllfile = '%s$(SO_EXT)' % self.dll_name
-        MakeRuleCmd.remove_installed_files(out, os.path.join('lib', dllfile))
+        MakeRuleCmd.remove_installed_files(out, os.path.join(INSTALL_LIB_DIR, dllfile))
         pythonPkgDirWithoutPrefix = strip_path_prefix(PYTHON_PACKAGE_DIR, PREFIX)
         MakeRuleCmd.remove_installed_files(out, os.path.join(pythonPkgDirWithoutPrefix, dllfile))
         libfile = '%s$(LIB_EXT)' % self.dll_name
-        MakeRuleCmd.remove_installed_files(out, os.path.join('lib', libfile))
+        MakeRuleCmd.remove_installed_files(out, os.path.join(INSTALL_LIB_DIR, libfile))
 
     def mk_win_dist(self, build_path, dist_path):
         if self.install:
-            mk_dir(os.path.join(dist_path, 'bin'))
+            mk_dir(os.path.join(dist_path, INSTALL_BIN_DIR))
             shutil.copy('%s.dll' % os.path.join(build_path, self.dll_name),
-                        '%s.dll' % os.path.join(dist_path, 'bin', self.dll_name))
+                        '%s.dll' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name))
             shutil.copy('%s.lib' % os.path.join(build_path, self.dll_name),
-                        '%s.lib' % os.path.join(dist_path, 'bin', self.dll_name))
+                        '%s.lib' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name))
 
     def mk_unix_dist(self, build_path, dist_path):
         if self.install:
-            mk_dir(os.path.join(dist_path, 'bin'))
+            mk_dir(os.path.join(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, 'bin', self.dll_name), so))
+                        '%s.%s' % (os.path.join(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, 'bin', self.dll_name))
+                        '%s.a' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name))
 
 class DotNetDLLComponent(Component):
     def __init__(self, name, dll_name, path, deps, assembly_info_dir):
@@ -1329,14 +1336,14 @@ class DotNetDLLComponent(Component):
     def mk_win_dist(self, build_path, dist_path):
         if DOTNET_ENABLED:
             # Assuming all DotNET dll should be in the distribution
-            mk_dir(os.path.join(dist_path, 'bin'))
+            mk_dir(os.path.join(dist_path, INSTALL_BIN_DIR))
             shutil.copy('%s.dll' % os.path.join(build_path, self.dll_name),
-                        '%s.dll' % os.path.join(dist_path, 'bin', self.dll_name))
+                        '%s.dll' % os.path.join(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, 'bin', self.dll_name))
+                        '%s.xml' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name))
             if DEBUG_MODE:
                 shutil.copy('%s.pdb' % os.path.join(build_path, self.dll_name),
-                            '%s.pdb' % os.path.join(dist_path, 'bin', self.dll_name))
+                            '%s.pdb' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name))
 
 
 
@@ -1406,36 +1413,36 @@ class JavaDLLComponent(Component):
 
     def mk_win_dist(self, build_path, dist_path):
         if JAVA_ENABLED:
-            mk_dir(os.path.join(dist_path, 'bin'))
+            mk_dir(os.path.join(dist_path, INSTALL_BIN_DIR))
             shutil.copy('%s.jar' % os.path.join(build_path, self.package_name),
-                        '%s.jar' % os.path.join(dist_path, 'bin', self.package_name))
+                        '%s.jar' % os.path.join(dist_path, INSTALL_BIN_DIR, self.package_name))
             shutil.copy(os.path.join(build_path, 'libz3java.dll'),
-                        os.path.join(dist_path, 'bin', 'libz3java.dll'))
+                        os.path.join(dist_path, INSTALL_BIN_DIR, 'libz3java.dll'))
             shutil.copy(os.path.join(build_path, 'libz3java.lib'),
-                        os.path.join(dist_path, 'bin', 'libz3java.lib'))
+                        os.path.join(dist_path, INSTALL_BIN_DIR, 'libz3java.lib'))
 
     def mk_unix_dist(self, build_path, dist_path):
         if JAVA_ENABLED:
-            mk_dir(os.path.join(dist_path, 'bin'))
+            mk_dir(os.path.join(dist_path, INSTALL_BIN_DIR))
             shutil.copy('%s.jar' % os.path.join(build_path, self.package_name),
-                        '%s.jar' % os.path.join(dist_path, 'bin', self.package_name))
+                        '%s.jar' % os.path.join(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, 'bin', 'libz3java.%s' % so))
+                        os.path.join(dist_path, INSTALL_BIN_DIR, 'libz3java.%s' % so))
 
     def mk_install(self, out):
         if is_java_enabled() and self.install:
             dllfile = '%s$(SO_EXT)' % self.dll_name
-            MakeRuleCmd.install_files(out, dllfile, os.path.join('lib', dllfile))
+            MakeRuleCmd.install_files(out, dllfile, os.path.join(INSTALL_LIB_DIR, dllfile))
             jarfile = '{}.jar'.format(self.package_name)
-            MakeRuleCmd.install_files(out, jarfile, os.path.join('lib', jarfile))
+            MakeRuleCmd.install_files(out, jarfile, os.path.join(INSTALL_LIB_DIR, jarfile))
 
     def mk_uninstall(self, out):
         if is_java_enabled() and self.install:
             dllfile = '%s$(SO_EXT)' % self.dll_name
-            MakeRuleCmd.remove_installed_files(out, os.path.join('lib', dllfile))
+            MakeRuleCmd.remove_installed_files(out, os.path.join(INSTALL_LIB_DIR, dllfile))
             jarfile = '{}.jar'.format(self.package_name)
-            MakeRuleCmd.remove_installed_files(out, os.path.join('lib', jarfile))
+            MakeRuleCmd.remove_installed_files(out, os.path.join(INSTALL_LIB_DIR, jarfile))
 
 class MLComponent(Component):
     def __init__(self, name, lib_name, path, deps):
@@ -2034,9 +2041,9 @@ def mk_install(out):
     if is_ml_enabled() and OCAMLFIND != '':
         out.write('ocamlfind_install')
     out.write('\n')
-    MakeRuleCmd.make_install_directory(out, 'bin')
-    MakeRuleCmd.make_install_directory(out, 'include')
-    MakeRuleCmd.make_install_directory(out, 'lib')
+    MakeRuleCmd.make_install_directory(out, INSTALL_BIN_DIR)
+    MakeRuleCmd.make_install_directory(out, INSTALL_INCLUDE_DIR)
+    MakeRuleCmd.make_install_directory(out, INSTALL_LIB_DIR)
     pythonPkgDirWithoutPrefix = strip_path_prefix(PYTHON_PACKAGE_DIR, PREFIX)
     MakeRuleCmd.make_install_directory(out, pythonPkgDirWithoutPrefix)
     for c in get_components():
@@ -2055,7 +2062,7 @@ def mk_install(out):
         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, 'lib'), LD_LIBRARY_PATH))
+                  (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)
     out.write('\n')
 
@@ -3206,7 +3213,7 @@ def mk_win_dist(build_path, dist_path):
     print("Adding to %s\n" % dist_path)
     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, 'bin', pyc))
+                    os.path.join(dist_path, INSTALL_BIN_DIR, pyc))
 
 def mk_unix_dist(build_path, dist_path):
     for c in get_components():
@@ -3214,7 +3221,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, 'bin', pyc))
+                    os.path.join(dist_path, INSTALL_BIN_DIR, pyc))
 
 class MakeRuleCmd(object):
     """

From 6884d3a245d59e7f8c02133c1ffa1fc2b60061b3 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Sat, 5 Dec 2015 07:50:33 +0000
Subject: [PATCH 15/15] Fix references to non existent function and variable
 due to a refactor in 041c02feb7aa682ecc887a2a1064b5729c68a5b4. Spotted by
 @NikolajBjorner

---
 scripts/mk_util.py | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index d7021b570..3e5590d5e 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -671,12 +671,11 @@ def parse_options():
     # Handle the Python package directory
     if not IS_WINDOWS:
         if not PYTHON_PACKAGE_DIR.startswith(PREFIX):
-            printPythonPackageMessage("ERROR")
             print(("ERROR: The detected Python package directory (%s)"
                    " does not live under the installation prefix (%s)"
                    ". This would lead to a broken installation."
                    "Use --pypkgdir= to change the Python package directory") %
-                  (errorType, PYTHON_PACKAGE_DIR, PREFIX))
+                  (PYTHON_PACKAGE_DIR, PREFIX))
             sys.exit(1)
 
 # Return a list containing a file names included using '#include' in