diff --git a/examples/ml/README b/examples/ml/README index 3e1eb0d1c..f934aac80 100644 --- a/examples/ml/README +++ b/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 \ No newline at end of file diff --git a/scripts/mk_util.py b/scripts/mk_util.py index d4221c05e..f6f95cf7d 100644 --- a/scripts/mk_util.py +++ b/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() diff --git a/src/api/ml/README b/src/api/ml/README index beee7d864..f697e5ff4 100644 --- a/src/api/ml/README +++ b/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. \ No newline at end of file +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. \ No newline at end of file