OCaml bindings fail to build in some environments

[vbgl]

The following line is erroneous:

z3/scripts/mk_util.py

Line 1998 in d5cc162

stubs_install_path = '$$(%s printconf path)/stublibs' % OCAMLFIND

The command ocamlfind printconf path outputs a list of paths separated by line feeds (see the documentation of ocamlfind). So when there are several elements in this list, appending /stublibs to it produces garbage.

I’ve tried a few successful patches in my environment but I don’t understand this code enough to propose something that makes sense in general.

[NikolajBjorner]

I can't help you based on the information. Maybe someone has bandwidth/skills to know, but otherwise we will have to punt on this.

While on the topic, the automatic build has been shown to be flaky.

It sometimes produces errors of the form.

Z3 was successfully built.
Z3Py scripts can already be executed in the 'build/python' directory.
Z3Py scripts stored in arbitrary directories can be executed if the 'build/python' directory is added to the PYTHONPATH environment variable and the 'build' directory is added to the LD_LIBRARY_PATH environment variable.
Use the following command to install Z3 at prefix /usr.
    sudo make install
ocamlfind ocamlc -o  ml_example_static.byte -thread -package z3-static -linkpkg  ../examples/ml/ml_example.ml
ocamlfind ocamlc -custom -o  ml_example_static_custom.byte -thread -package z3-static -linkpkg  ../examples/ml/ml_example.ml
ocamlfind ocamlopt -o  ml_example_static -thread -package z3-static -linkpkg  ../examples/ml/ml_example.ml
File "../examples/ml/ml_example.ml", line 1:
Error: The file ../examples/ml/ml_example.cmo is not a bytecode object file
make: *** [Makefile:5033: ml_example_static.byte] Error 2
make: *** Waiting for unfinished jobs....

Appears not directly related.

[vbgl]

There might be a misunderstanding: I’m not asking for help. I just wanted to let you know that there is a bug in your software.

[vbgl]

FTR, here is my workaround:

diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 042e6af46..1e105b002 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -1995,7 +1995,7 @@ class MLComponent(Component):
 
             LIBZ3 = LIBZ3 + ' ' + ' '.join(map(lambda x: '-cclib ' + x, LDFLAGS.split()))
 
-            stubs_install_path = '$$(%s printconf path)/stublibs' % OCAMLFIND
+            stubs_install_path = '$$(%s printconf destdir)/stublibs' % OCAMLFIND
             if not STATIC_LIB:
                 loadpath = '-ccopt -L' + stubs_install_path
                 dllpath = '-dllpath ' + stubs_install_path

[vbgl]

This has been fixed by 4f6fcf8 (after being reported again in #5814).