Added facilities for ocamlfind in the ML API build

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>

examples/ml/README

@@ -1,4 +1,4 @@
-### This is work-in-progress and does not work yet.
+### This is work-in-progress.
 
 Small example using the Z3 ML bindings.
 To build the example execute
@@ -12,3 +12,13 @@ or
 LD_LIBRARY_PATH=. ./ml_example.byte
 for the byte-code version.
 
+If Z3 was installed into the ocamlfind package repository (see src/api/ml/README),
+then we can compile this example as follows:
+
+ocamlfind ocamlc -o ml_example.byte -custom -package Z3 -linkpkg -verbose
+ocamlfind ocamlopt -o ml_example -package Z3 -linkpkg -verbose
+
+Note that the resulting binaries depend on the shared z3 library, which needs to be 
+in the PATH (Windows), LD_LIBRARY_PATH (Linux) or DYLD_LIBRARY_PATH (OSX). If Z3 was 
+installed into ocamlfind, the path that should be added is 
+`ocamlfind printconf destdir`/Z3

scripts/mk_util.py

@@ -1338,7 +1338,25 @@ class MLComponent(Component):
         Component.__init__(self, name, path, deps)
         if lib_name == None:
             lib_name = name
-        self.lib_name     = lib_name
+        self.lib_name = lib_name
+
+    def mk_ml_meta(self, ml_meta_in, ml_meta_out, major, minor, build, revision):
+        ver_pat   = re.compile('version = "VERSION"*')
+        fin  = open(ml_meta_in, 'r')
+        fout = open(ml_meta_out, 'w')
+        num_updates = 0
+        for line in fin:
+            if ver_pat.match(line):
+                fout.write('version = "%s.%s.%s.%s"\n' % (major, minor, build, revision))
+                num_updates = num_updates + 1
+            else:
+                fout.write(line)
+        assert num_updates == 1, "unexpected number of version number updates"
+        fin.close()
+        fout.close()
+        if VERBOSE:
+            print("Updated '%s'" % ml_meta_out)
+                        
 
     def mk_makefile(self, out):
         if is_ml_enabled():
@@ -1377,7 +1395,7 @@ class MLComponent(Component):
             out.write('api/ml/libz3ml$(LIB_EXT): api/ml/z3native.c %s$(SO_EXT)\n' % get_component(Z3_DLL_COMPONENT).dll_name)
             out.write('\t$(CXX) $(CXXFLAGS) -I %s -I %s %s/z3native.c $(CXX_OUT_FLAG)api/ml/z3native$(OBJ_EXT)\n' % (OCAML_LIB, api_src, sub_dir))
             out.write('\t$(AR) $(AR_FLAGS) $(AR_OUTFLAG)api/ml/libz3ml$(LIB_EXT) api/ml/z3native$(OBJ_EXT)\n')
-            out.write('api/ml/z3.cmxa: api/ml/libz3ml$(LIB_EXT) %s$(SO_EXT) %s' % (get_component(Z3_DLL_COMPONENT).dll_name, cmis))
+            out.write('%s: api/ml/libz3ml$(LIB_EXT) %s$(SO_EXT) %s' % (os.path.join(sub_dir, 'z3.cmxa'), get_component(Z3_DLL_COMPONENT).dll_name, cmis))
             for mlfile in get_ml_files(self.src_dir):
                 out.write(' %s' % os.path.join(sub_dir, mlfile))
             out.write('\n')
@@ -1385,7 +1403,7 @@ class MLComponent(Component):
             if DEBUG_MODE:
                 out.write('-g ')
             out.write('-cclib "-L../.. -lz3ml" -I %s %s/z3enums.ml %s/z3native.ml %s/z3.ml -a -o api/ml/z3.cmxa -linkall\n' % (sub_dir,sub_dir,sub_dir,sub_dir))
-            out.write('api/ml/z3.cma: api/ml/libz3ml$(LIB_EXT) %s$(SO_EXT) %s' % (get_component(Z3_DLL_COMPONENT).dll_name, cmis))
+            out.write('%s: api/ml/libz3ml$(LIB_EXT) %s$(SO_EXT) %s' % (os.path.join(sub_dir, 'z3.cma'), get_component(Z3_DLL_COMPONENT).dll_name, cmis))
             for mlfile in get_ml_files(self.src_dir):
                 out.write(' %s' % os.path.join(sub_dir, mlfile))
             out.write('\n')
@@ -1395,6 +1413,13 @@ class MLComponent(Component):
             out.write('-cclib "-L../.. -lz3ml" -I %s %s/z3enums.ml %s/z3native.ml %s/z3.ml -a -o api/ml/z3.cma -linkall\n' % (sub_dir,sub_dir,sub_dir,sub_dir))
             out.write('ml: api/ml/z3.cmxa api/ml/z3.cma\n')
             out.write('\n')
+            # Generate META file and package installation commands
+            self.mk_ml_meta(os.path.join('src/api/ml/META'), os.path.join(BUILD_DIR, sub_dir, 'META'), VER_MAJOR, VER_MINOR, VER_BUILD, VER_REVISION)
+            out.write('ocamlfind_install: api/ml/z3.cma api/ml/z3.cmxa\n')
+            out.write('\tocamlfind remove Z3\n')
+            out.write('\tocamlfind install Z3 api/ml/META api/ml/z3.cma api/ml/z3.cmxa api/ml/z3.lib api/ml/libz3ml.lib libz3.lib libz3.dll\n')
+            out.write('\n')
+
     
     def main_component(self):
         return is_ml_enabled()

src/api/ml/README

@@ -5,4 +5,8 @@ We are currently working on a brand new ML API.
 On Windows, there are no less than four different ports of OCaml. The Z3 build 
 system assumes that either the win32 or the win64 port is installed. This means
 that OCaml will use `cl' as the underlying C compiler and not the cygwin or
-mingw compilers. 
+mingw compilers. 
+
+By default, a make target called `ocamlfind_install' is added. This installs Z3
+into the ocamlfind package repository such that programs can be compiled via 
+ocamlfind.