However, the file libz3.dylib is in ~/.opam/myswitch/z3/libz3.dylib . So I need to extend my DYLD_LIBRARY_PATH or LD_LIBRARY_PATH or PATH depending on my operating system. And I want that to be done dynamically depending on the current switch/esy sandbox I’m using Is there a way of doing that properly with dune ?
Also, is it possible to point to the said dylib file so that it gets added to the .install file ?
We’re building both a binary and a library, and because of z3, any binary built with our library will need the dylib file… And if the binary is installed, it needs to be installed next to the dylib file. I wish there was a way to get rid of that file and integrate it in the ocaml z3 library directly…
Also if there was a way just juste statically include libz3.dylib into my final binary/library that would be actually simpler, but I don’t know if that’s possible
Usually, such libraries are statically linked into native OCaml executables. It’s only C libraries installed system-wide that are dynamically loaded. For bytecode OCaml executables, they are commonly dynamically loaded, however the dynamic libraries are installed at a central place.
z3 seems to use an ad-hoc build, so it is a bit hard to say how it is meant to be used. Do you know if they have some documentation somewhere that explain how it is supposed to be used? That would help find out how it can be used in a dune project.
Thanks for your answer. I pushed a little deeper into the subject, and I asked directly to the z3 team.
They don’t maintain the opam package, someone else does. (From Aesthetic Integration, which seems to be cloud-native stuff, so I guess that they have a custom way of distributing the dylib).
The only “official” way of using z3 is with a global install, which is ok for using the tool on our end, but if we ever decide to distribute the tool, will become quite annoying.
My current approach is to try and make an esy package out of z3 (thanks to an advice from the OCaml discord). I think it will work (I can’t be sure yet, I’m having some small issues in the process).
However, that will make me esy-dependant, meaning I will not be able to deploy anything on opam.
An ideal solution would be to “fix” the opam z3 version so that it installs the libz3 “at the right place”, but I guess this is more of an opam issue than a dune issue. I don’t really know if there’s a way to do that properly without breaking some of the interesting properties of opam.
Well z3’s ocaml bindings come with the main source code, using a very complicated build script in python (there’s an ongoing effort to port to cmake but the OCaml bindings part is not done yet). It’s not a simple case that would fit dune, imho. Using the .a instead of .so might be possible but it’s beyond my (basic) skills in linking/packaging.
Yes, I have reached the same conclusion I think
I eventually decided on using the opam version of z3 and having a esy init script that copies the dylib in the right place. That can be done easily because esy knows at any where z3 lives. A pure-opam version would include some ocamlfind I guess.