Z3 build scripts assume there's a single ocamlfind path location

[protz]

This assumes the output of ocamlfind printconf path is a single entry:

z3/scripts/mk_util.py

Line 1998 in 4749495

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

This is incorrect: the user may export OCAMLPATH to inform ocamlfind that there are multiple directories in which to find packages. For instance, on my machine:

jonathan@absinthe:~/Code/z3 (master) $ ocamlfind printconf path
/Users/jonathan/Code/everest/fstar/bin
/Users/jonathan/.opam/default/lib

This generates an incorrect ocamlmklib invocation:

ocamlmklib -o api/ml/z3ml -I api/ml -L. api/ml/z3native_stubs.o api/ml/z3enums.cmo api/ml/z3native.cmo api/ml/z3.cmo -lz3 -lstdc++ -ccopt -L/Users/jonathan/Code/everest/fstar/bin /Users/jonathan/.opam/default/lib/stublibs -dllpath /Users/jonathan/Code/everest/fstar/bin /Users/jonathan/.opam/default/lib/stublibs

which in turn makes the build fail:

ocamlmklib -o api/ml/z3ml  -I api/ml -L. api/ml/z3native_stubs.o api/ml/z3enums.cmo api/ml/z3native.cmo api/ml/z3.cmo  -lz3 -lstdc++  -ccopt -L$(ocamlfind printconf path)/stublibs -dllpath $(ocamlfind printconf path)/stublibs
Don't know what to do with /Users/jonathan/.opam/default/lib/stublibs

Proposed patch:

diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 042e6af46..e3319c257 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 path | tail -n 1)/stublibs' % OCAMLFIND
             if not STATIC_LIB:
                 loadpath = '-ccopt -L' + stubs_install_path
                 dllpath = '-dllpath ' + stubs_install_path

Thanks,

Jonathan

[NikolajBjorner]

Are you going to add a pull request or asking for more input?

[protz]

If you're ok with my analysis feel free to go ahead and commit the patch :-).

[NikolajBjorner]

@k4rtik - what do you think about the patch from this sketchy character?

[k4rtik]

I think we are really calling in @arbipher here to look at this. See #5617 where these changes were last made.

But since I already spent some time looking at it, how would we know that the last entry is the correct entry for stublibs? The patch needs to be made more resilient or the right path determined without reliance on printconf path. I don't know how for either.

[arbipher]

I agree this may cause problems. I didn't notice ocamlfind printconf path can have multiple result, as shown in your case.
I check with ocamlfind manual and src (List.iter print_endline (Findlib.search_path())). There is no argument to filter just one result for ocamlfind printconf path.

My previous fix uses the path to find stublibs and the path it's used for linking. I would also ask K4rtik's question and then I found the answer. I test it on my own (by export OCAMLPATH and see the result of the command).
I have spent some time to read its source of ocamlfind, the result of the command comes from env_search_path @ sys_search_path (src) where:

• env_search_path is set by reading OCAMLPATH.
• sys_search_path is the path defined in the findlib config file. See this comment.

The conf file can be found by ocamlfind printconf conf.

$ cat /home/exx/.opam/4.13.1/lib/findlib.conf
destdir="/home/exx/.opam/4.13.1/lib"
path="/home/exx/.opam/4.13.1/lib"
ocamlc="ocamlc.opt"

I am thinking since the task is to get the path ocamlfind install uses destdir in the conf file, maybe we could use ocamlfind printconf destdir instead. destdir should be just one path (manual).

Then the patch will be this at the line

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

[k4rtik]

Perfect, destdir does seem like an appropriate solution. Excellent analysis, @arbipher!

[protz]

Thanks for the improved solution -- best not to trust patches from sketchy characters indeed!

[NikolajBjorner]

and meanwhile...

[arbipher]

lol, as the current maintainer of the z3-ocaml on opam, I know two faces in the photo!