diff --git a/examples/ml/README b/examples/ml/README index 04837c696..1c474fe33 100644 --- a/examples/ml/README +++ b/examples/ml/README @@ -1,20 +1,23 @@ Small example using the Z3 ML bindings. + To build the example execute make examples in the build directory. -It will create ml_example in the build directory, -which can be run in the build directory via +This will create ml_example and ml_example.byte in the build directory, which +can be run in the build directory by calling LD_LIBRARY_PATH=. ./ml_example 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: +If Z3 was installed into the ocamlfind package repository (see +src/api/ml/README), then we can also compile this example as follows: ocamlfind ocamlc -o ml_example.byte -package Z3 -linkpkg ml_example.ml +or ocamlfind ocamlopt -o ml_example -package Z3 -linkpkg ml_example.ml -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). +Note that the resulting binaries depend on the shared z3 library +(libz3.dll/.so/.dylb), which needs to be in the PATH (Windows), LD_LIBRARY_PATH +(Linux), or DYLD_LIBRARY_PATH (OSX). diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 4b3a1aeaa..9d58bea3f 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -1750,7 +1750,11 @@ class MLComponent(Component): api_src = get_component(API_COMPONENT).to_src_dir out.write('CXXFLAGS_OCAML=$(CXXFLAGS:/GL=)\n') # remove /GL; the ocaml tools don't like it. - substitutions = { 'PREFIX': PREFIX, + if IS_WINDOWS: + prefix_lib = '-L' + os.path.abspath(BUILD_DIR).replace('\\', '\\\\') + else: + prefix_lib = '-L' + PREFIX + '/lib' + substitutions = { 'LEXTRA': prefix_lib, 'VERSION': "{}.{}.{}.{}".format(VER_MAJOR, VER_MINOR, VER_BUILD, VER_REVISION) } configure_file(os.path.join(self.src_dir, 'META.in'), @@ -1768,10 +1772,11 @@ class MLComponent(Component): out.write('\t%s -ccopt "$(CXXFLAGS_OCAML) -I %s -I %s -I %s $(CXX_OUT_FLAG)%s" -c %s\n' % (OCAMLC, OCAML_LIB, api_src, src_dir, stubso, stubsc)) + cmis = '' for m in self.modules: ff = os.path.join(src_dir, m + '.mli') ft = os.path.join(self.sub_dir, m + '.cmi') - out.write('%s: %s\n' % (ft, mlis)) + out.write('%s: %s %s\n' % (ft, mlis, cmis)) out.write('\t%s -I %s -o %s -c %s\n' % (OCAMLC, self.sub_dir, ft, ff)) cmos = '' @@ -1805,6 +1810,16 @@ class MLComponent(Component): out.write('ml: %s.cma %s.cmxa %s.cmxs\n' % (z3mls, z3mls, z3mls)) out.write('\n') + if IS_WINDOWS: + out.write('ocamlfind_install: ') + self.mk_install_deps(out) + out.write('\n') + self.mk_install(out) + out.write('\n') + out.write('ocamlfind_uninstall:\n') + self.mk_uninstall(out) + out.write('\n') + def mk_install_deps(self, out): if is_ml_enabled() and OCAMLFIND != '': out.write(get_component(Z3_DLL_COMPONENT).dll_name + '$(SO_EXT) ') diff --git a/src/api/ml/META.in b/src/api/ml/META.in index 6f4638749..1951e60b3 100644 --- a/src/api/ml/META.in +++ b/src/api/ml/META.in @@ -5,7 +5,7 @@ requires = "num" archive(byte) = "z3ml.cma" archive(native) = "z3ml.cmxa" archive(byte,plugin) = "z3ml.cma" -archive(native,plugin) = "z3ml.cmxa" +archive(native,plugin) = "z3ml.cmxs" archive(byte,toploop) = "z3ml.cma" archive(native,toploop) = "z3ml.cmxa" -linkopts = "-cclib -L@PREFIX@/lib -cclib -lz3" +linkopts = "-cclib @LEXTRA@" diff --git a/src/api/ml/README b/src/api/ml/README index ffdd3e709..c2750594a 100644 --- a/src/api/ml/README +++ b/src/api/ml/README @@ -4,8 +4,10 @@ refer to previous releases of Z3. 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. \ No newline at end of file +OCamlfind: When ocamlfind is found, the `install' target will install the Z3 +OCaml bindings into the ocamlfind site-lib directory. The installed package is +linked against the (dynamic) libz3 and it adds $(PREFIX)/lib to the library +include paths. On Windows, there is no $(PREFIX), so the build directory is +used instead (see META.in).