From 9bb0c882faca510165a546e1a7ed2024d2470894 Mon Sep 17 00:00:00 2001
From: Louis Gesbert <louis.gesbert@ocamlpro.com>
Date: Tue, 21 May 2019 17:44:19 +0200
Subject: [PATCH] OCaml API build: provide static linking options by default

when --staticlib is enabled, the linker will still choose to
dynamically link upon encountering `-lz3` when generating an
executable through OCaml.

The interaction between the underlying C linker and OCaml make it very
hard to choose the static version instead. The present patch works
around this issue by copying `libz3.a` to `libz3-static.a`, and using
`-lz3-static` instead: the static version is chosen since no dynamic
one is found.

One can get back to dynamically linking by compiling without
`--staticlib`, or switching back to `-lz3`, but will in the latter
case run into the same problem with specifying the option; if that
needs to be made easier, we could provide two versions of the `cm(x)a`
which differ only by their linking options.

One last solution would be to remove `lz3` altogether from the linking
options included in the cm(x)a, requiring either `-lz3` or
`-lz3-static` to be specified at link time. Simpler and most flexible,
but requires an update of all users that link with the Z3 ml api...
---
 scripts/mk_util.py | 21 +++++++++++++++------
 1 file changed, 15 insertions(+), 6 deletions(-)

diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index f076817d2..2716052c0 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -2221,8 +2221,16 @@ class MLComponent(Component):
 
             stubsc = os.path.join(src_dir, self.stubs + '.c')
             stubso = os.path.join(self.sub_dir, self.stubs) + '$(OBJ_EXT)'
-            z3dllso = get_component(Z3_DLL_COMPONENT).dll_name + '$(SO_EXT)'
-            out.write('%s: %s %s\n' % (stubso, stubsc, z3dllso))
+            base_dll_name = get_component(Z3_DLL_COMPONENT).dll_name
+            if STATIC_LIB:
+                z3link = 'z3-static'
+                z3linkdep = base_dll_name + '-static$(LIB_EXT)'
+                out.write('%s: %s\n' % (z3linkdep, base_dll_name + '$(LIB_EXT)'))
+                out.write('\tcp $< $@\n')
+            else:
+                z3link = 'z3'
+                z3linkdep = base_dll_name + '$(SO_EXT)'
+            out.write('%s: %s %s\n' % (stubso, stubsc, z3linkdep))
             out.write('\t%s -ccopt "$(CXXFLAGS_OCAML) -I %s -I %s -I %s $(CXX_OUT_FLAG)%s" -c %s\n' %
                       (OCAMLCF, OCAML_LIB, api_src, src_dir, stubso, stubsc))
 
@@ -2253,9 +2261,9 @@ class MLComponent(Component):
 
             OCAMLMKLIB = 'ocamlmklib'
 
-            LIBZ3 = '-lz3'
+            LIBZ3 = '-l' + z3link
             if is_cygwin() and not(is_cygwin_mingw()):
-                LIBZ3 = 'libz3.dll'
+                LIBZ3 = z3linkdep
 
             LIBZ3 = LIBZ3 + ' ' + ' '.join(map(lambda x: '-cclib ' + x, LDFLAGS.split()))
 
@@ -2264,9 +2272,10 @@ class MLComponent(Component):
                 OCAMLMKLIB += ' -g'
 
             z3mls = os.path.join(self.sub_dir, 'z3ml')
-            out.write('%s.cma: %s %s %s\n' % (z3mls, cmos, stubso, z3dllso))
+
+            out.write('%s.cma: %s %s %s\n' % (z3mls, cmos, stubso, z3linkdep))
             out.write('\t%s -o %s -I %s %s %s %s\n' % (OCAMLMKLIB, z3mls, self.sub_dir, stubso, cmos, LIBZ3))
-            out.write('%s.cmxa: %s %s %s %s.cma\n' % (z3mls, cmxs, stubso, z3dllso, z3mls))
+            out.write('%s.cmxa: %s %s %s %s.cma\n' % (z3mls, cmxs, stubso, z3linkdep, z3mls))
             out.write('\t%s -o %s -I %s %s %s %s\n' % (OCAMLMKLIB, z3mls, self.sub_dir, stubso, cmxs, LIBZ3))
             out.write('%s.cmxs: %s.cmxa\n' % (z3mls, z3mls))
             out.write('\t%s -linkall -shared -o %s.cmxs -I . -I %s %s.cmxa\n' % (OCAMLOPTF, z3mls, self.sub_dir, z3mls))