OCaml installation is broken about z3 HOT 27 CLOSED

That could work, but only in theory. It would require a major rewrite of the ML API and some other parts of Z3 as well. Also, there would be no consistency between multiple different APIs installed on the same system, because they would use different copies of Z3 (compiled with different flags, static vs dynamic, etc). If it's really necessary, we could try to think about linking libz3 statically into libz3ml.so, only when the --staticlib option is on to keep it local for now (the build is probably broken in that case anyways).

If it can't find libz3.so which is properly installed into your ocamlfind directory, it probably means that your (DY)LD_LIBRARY_PATH isn't set up properly or ldconfig needs to be run? The directory reported by echo ocamlfind printconf destdir/Z3 should contain libz3.so/.dylib.

from z3.

The directory reported by echo ocamlfind printconf destdir/Z3 should contain libz3.so/.dylib.

That's not true for me, they are installed in `` ocamlfind printconf destdir/stublibs.

from z3.

Interesting... did they change the default paths yet again? What version of ocamlfind are you using?

from z3.

I don't think they changed it. I'm using version 1.5.5. (and opam, but not sure if it should change anything, @AltGr ?)

from z3.

Note that changing the directory doesn't really help. OCamlers don't usually have their LD_LIBRARY_PATH setup that way, so it would need additional setup from the user, which is sub-optimal.

Ok so, the situation from the ocaml perspective (and in particular, the desire to package z3 and its API in opam, the usual package manager for ocaml which is a source package manager) is, as far as I can see the following:

• if distribs don't package z3 (and they don't for now, but I expect it to change) a z3 opam package have to recompile z3 in a whole and so the package will contains its own version of libz3.so, hence linking statically in libz3ml seems acceptable to me. This means long-ish compilation time, but is very flexible.
• if distribs do start packaging z3, they will probably don't distribute the ml package (and it's preferable to have it in opam anyway, to handle multiple ocaml versions). In this case, dynamic linking against the system z3 is the preferable way, but in this case, it would be much more convenient to be able to recompile the ml binding against a system z3 (instead of recompiling libz3.so before, as it's done currently). This is how llvm in-tree bindings are packaged in opam currently. This means installing dev versions is a bit of a sport but makes the package very fast to compile.

I'm personally fine with either solution (both have great merits) but you need to choose one. The current state is slightly sitting in the middle and is very inappropriate for separate packaging of z3 and the ml API.

Note that I don't ask you to officially support opam or any package manager in any way, just give a way to package it cleanly. ;)

How does that sounds ? I'm sorry for being a bit insistent about it, I just want to distribute packages depending on z3 to my fellow ocamlers. :D

from z3.

Ping ? :)

from z3.

Pong.

from z3.

We are now getting close to a state where we should think about this issue again. In all other settings, Z3 is a native code, shared library, which is linked to by applications of the various languages/systems. What would be the preferred way for OCaml users to access a library of that type? I had a quick look but I couldn't find anything of that type in the OPAM repository. Do they rely on the system package manager to install such libraries?

From my perspective, I think the best way to handle this issue would be to compile and install a custom Z3 during OPAM installation, except if a libz3.so of the right version is found in the LD_LIBRARY_PATH, similar to your second suggestion. We can add a custom flag or a separate OPAM package called z3-dev or similar to make it easier to get everything set up for development which will always compile the latest version, etc.

I expect that at least some popular systems will get Z3 packages (e.g., Michael Tauschnig has started publishing packages for Debian testing and unstable).

from z3.

llvm is quite similar to z3 in this regard. The opam package relies on the system's llvm and compiles only the OCaml bits.

from z3.

Bumping this. I still think we should rely on the system package manager to install the shared library or on make install of Z3. We also have the --static-lib flag on mk_make.py and we could try to build a statically linked libz3ml.so (or .a?) when that's enabled. Z3 being what it is, I expect most users to be developers of some sort, so they will know what they want to use and whether they have Z3 installed and which version they want to use.

I think the original questions was answered elsewhere - the distribution paths are not the same on all platforms, that's why libz3.so wasn't found.

What's the status of the current OPAM package, is that in some way alive?

from z3.

I have a version of the opam packages that works in this repository. I agree with the system Z3.

Last time I tried, bytecode was still broken.

from z3.

Can you remind me what's broken in the bytecode compilation? Was that the toplevel problem which I think was resolved?

from z3.

Yes, it's the toplevel issue. The error message is :

Error: The external function `n_is_null' is not available       

It was indeed solved at some point, then it broke again.

from z3.

Right, I took another look at this and refactored the build a little bit.

The core of the problem is that the ocaml toplevel does not support dynamic linking and the -custom option on ocamlmklib doesn't add a custom runtime, but it simply disables dynamic linking. I remember getting the toplevel to work at some point, but I have no recollection of how I did that; it's quite possible I played around with static libraries at the time.

Here are some options:

• Add optional static libraries and make it a requirement for the ML API, or
• automatically build a new toplevel that links Z3 dynamically, or
• don't support bytecode ocaml at all, only native, or
• figure out a way to load a shared object from the toplevel (hack ocamlrun?)
• anything else?

Assuming that some system package will install a shared object for z3 (libz3.so) it would be very confusing for users if there is another, static library which is used for bytecode, but not in native mode, as they would see different errors and solver behaviour if those two libraries aren't precisely matched. That's why I don't like the static route.

I like the custom toplevel way, but mostly because it's probably the least amount of work for me. I have no idea whether anyone would ever use it.

Not supporting bytecode is OK with me, but I guess there are some users who do use that at least for debugging.

If there's a way to teach the toplevel to load a shared object let me know, I couldn't find one so far, so I assume adding facilities for that would be quite a lot of work.

from z3.

The toplevel supports dynlink (many ocaml library do this, see zarith for gmp, for example).

I'm pretty sure you don't need a single thing of all that. I don't understand your build system, so I won't comment, but know that when I extracted the (generated) code of the binding and a trivial oasis file, everything worked, including toplevel. And it was still dynamically linked.

from z3.

Right, so there must be a command to load a .so then... can you point me towards that?

from z3.

But you shouldn't need to do that explicitly. the cma should contains all the linking informations.
I don't see why your problem is specific to the toplevel, your issue is with bytecode in general ...

from z3.

Yes that's correct, but the bytecode compiler has a -custom option to add the runtime, while ocamlmklib and the toplevel don't have that option.

from z3.

That's for static linking though, we only need dynamic linking here.

from z3.

No, that is only true for ocamlmklib (see help, it says disable dynamic linking), the meaning of -custom on ocamlc is completely different.

from z3.

I suppose it could potentially work if we use -custom on one part of the library and not use it on the other parts. I dimly remember that not being supported either though.

from z3.

Alright, I have just committed another set of fixes for the ocaml packages now without any -custom's. These packages work on all my systems in native/bytecode/toplevel and with ocaml 4.02.3, but I still consider them very brittle. They might not work with any other version of ocaml or on other systems than the one I tested this on.

Could you give this a try to see whether this works for you? @arlencox, @jberdine wanna give this a try too?

from z3.

My solution to this problem was to modify the META file in the following way:

Remove

linkopts = "-cclib -lz3"

Add

linkopts(byte) = "-custom -cclib -lz3"
linkopts(native) = "-cclib -lz3"

The good thing about this is it avoids the mess of trying to get this stuff included directly into the cma with ocamlmklib (which I find to be finicky and poorly documented) and places the burden on the findlib. Given that basically everyone uses findlib these days, I see no reason not to operate this way. The need for compiler argument inclusion in cma files is essentially gone.

Regardless, I'll have a look at what you've done when I get home tonight.

from z3.

Did you make it home?

from z3.

It was a long walk home, but I finally made it....

It appears to work on my system! I tried both native and byte-code compiled. I also tried both debug and non-debug builds. I also tried using from the top level. It worked in all situations.

My system is Mac OS X 10.11.2 with OCaml 4.02.1 and an opam install from a few months ago.

from z3.

Thanks, I will close this ticket then. If there are problems with OCaml they are more likely to be based on newer issues.

from z3.

Awesome, thanks for checking @arlencox!

from z3.