OCaml bindings don't install with cmake build system

[numinit]

Hi there,

We recently switched in nixpkgs to the CMake based build system, since we began having downstream dependencies of Z3 that required having CMake files installed: https://github.com/NixOS/nixpkgs/pull/415966

All the bindings install but the ocaml ones. If we set Z3_BUILD_OCAML_BINDINGS, the output doesn't get installed: see the comment here. https://github.com/NixOS/nixpkgs/pull/415966/files#diff-884ce4cd3f3d3b74237b65e09677782996be7b3f9d6437b71717f7c1ba5de3e7R90

Is this a currently known limitation of the CMake build, or a bug?

[numinit]

Oh, I see the WIP commit here:

https://github.com/Z3Prover/z3/commit/f7aec02503d5bc3e8b7947093a4c96aeab98257e

[NikolajBjorner]

@arbipher

[arbipher]

Oh, it's WIP. Let me finish it next week.

I have some unpushed commits and was working on the CI testing for an integration test with opam installation last month (then was interrupted by something at the university)

[numinit]

No worries, appreciate the work. Hopefully we'll be able to completely switch off the autotools build system for newer versions of Z3 :-)

[arbipher]

It should do and that's my plan. I also recall the current ocaml binding has some building error due to the changed APIs (when I compiled it last month), which I also plan to fix.

[arbipher]

Here is some update.

Now the z3 and the opam-z3 both build and run well on CI (z3 result, opam-z3 result).

For z3 source, I keep the cmake default linking argument i.e. @rpath/${SOVERSION}.{so_ext} and it's tested in building and CI. For macos, the testing all relies on setting DYLD_LIBRARY_PATH. It should be the safe choice and leave the work(burden) to package managers.

For opam-z3, I add a package z3.dev , which currently points to my forked z3. The macos installation will fix the dylib install_name_tool.

The problem can be solved by using cmake --install. However, the opam needs to use ocamlfind install ... to keep track of installed files for future removal. I need some understanding later.

I haven't made any PRs for them yet but they should be in good shape.

I confirmed the OCaml API warning still exists.

I am also interested to check compiling ocaml-z3 with an external libz3 provided by system package managers. I have an optional Z3_BUILD_EXTERNAL_LIBZ3 in building but I don't make CI for it yet.

[NikolajBjorner]

I confirmed the OCaml API warning still exists.

Is this a good or a bad thing. Is this a warning that is actionable?

[arbipher]

It's a bad thing, which means the OCaml datatype doesn't update with the latest C/C++ API, but it's also not in the OCaml document so I don't think real people will be bothered . I can fix it and also put them in the testing ML file later.

[NikolajBjorner]

should we close this as fixed?

[LordGrimmauld]

We might need https://github.com/Z3Prover/z3/pull/7698/commits/1f0fc27d23b4c14cfac10b300accc7436df0b868 (which is not yet part of a release) to make z3 work on darwin systems with nix. That said, we can trivially fetch that patch, the changes to cmake likely apply cleanly on the tagged 4.15.2 release. That mostly seems like a minor packaging thing to keep in mind. But, that too is merged. I'll have a poke updating to a full cmake build later this week / weekend and ideally comparing compile output binaries.

It seems (without doing thorough testing, just checking code changes) that our problems were addressed, i think it is fair to close this and open a new issue if something else pops up trying to incorporate this.

[arbipher]

I am not familiar with Nix yet, but I would be happy to know. If any related problem occurs, feel free to ping me.

I haven't made PR for opam z3.dev package yet. I haven't worked on opam-ci for a while, so I plan to check out their recent document or CI pipeline update first. But the old z3/ocaml/mac should work well on their old.

[NikolajBjorner]

so a reason to roll 4.15.3?

[LordGrimmauld]

As i said, it is trivial to fetch that patch, not a real problem. More frequent tags are always welcome, and i will certainly not stop you from creating a new tag, but it shouldn't be strictly necessary to get this on the way now.

[LordGrimmauld]

Hmm, how do you actually trigger the generation of ocaml bindings? I see the libz3_ocaml target, but i don't see relevant outputs in the build directory, and i also don't see a flag Z3_INSTALL_OCAML_BINDINGS like we have Z3_INSTALL_JAVA_BINDINGS. I am probably missing something?

[LordGrimmauld]

Actually, it seems the bindings still don't get installed? https://github.com/Z3Prover/z3/blob/f544dd4ab2cec2567405204d7c3ac4cbefd2d20c/src/api/ml/CMakeLists.txt#L285-L308 Now i am confused...

[arbipher]

The building of ocaml binding can be triggered https://github.com/Z3Prover/z3/blob/f544dd4ab2cec2567405204d7c3ac4cbefd2d20c/.github/workflows/ocaml.yaml#L78-L81

The relevant outputs should be in build/src/api/ml.

The installation of ocaml binding, in my current unpushed PR, is not performed by CMake. The installation will install both the z3 library and ocaml stub libs into the correct path (your opam switch lib and stubslib).

https://github.com/arbipher/opam-repository/blob/8b6c717409c5fae3229c40e4e103f913c1edd0de/packages/z3/z3.dev/opam#L25-L40

(my previous thought) To install an ocaml binding as an opam package, it's not that natural for me to put it inside cmake install. Since cmake will read the opam status and invoke ocaml tools ocamlfind install. Also, to make the installed library working for platform macos, it also needs to patch the install_name_tool thing. It's more natural that cmake build the library and opam decides how to install. I am not familiar with how packages should be installed for other general packages. I can fix it if necessary.

btw, the current ocaml binding has to build the libz3 from source, which doesn't look a good design. I will work on how to split it with a conf-z3 later.

[arbipher]

(Solved. See notes in the end) Here are some experiments for homebrew. The normal homebrew packages are prebuilt, but you can also build from source.

For normal z3 prebuild packages, I found the artifact in the log.

otool -L lib/libz3.4.15.dylib 
lib/libz3.4.15.dylib:
	@@HOMEBREW_PREFIX@@/opt/z3/lib/libz3.4.15.dylib (compatibility version 4.15.0, current version 4.15.2)
	/usr/lib/libc++.1.dylib (compatibility version 1.0.0, current version 1900.178.0)
	/usr/lib/libSystem.B.dylib (compatibility version 1.0.0, current version 1351.0.0)

@@HOMEBREW_PREFIX@@ will be replaced by the actual installation path when installed.

For build from source, a.k.a running brew reinstall --build-from-source --keep-tmp z3.

In the tmp build directory,

otool -L build/libz3.4.15.dylib
build/libz3.4.15.dylib:
	@rpath/libz3.4.15.dylib (compatibility version 4.15.0, current version 4.15.2)
	/usr/lib/libc++.1.dylib (compatibility version 1.0.0, current version 1900.180.0)
	/usr/lib/libSystem.B.dylib (compatibility version 1.0.0, current version 1351.0.0)

@rpath/libz3.4.15.dylib is the default output path from cmake

If I follow the z3 formula (https://github.com/Homebrew/homebrew-core/blob/96987271b9c6c68e20ec64f820922e1c0ac76849/Formula/z/z3.rb#L60) to run cmake --install build at the tmp build, I will get:

otool -L /opt/homebrew/Cellar/z3/4.15.2/lib/libz3.4.15.2.0.dylib
/opt/homebrew/Cellar/z3/4.15.2/lib/libz3.4.15.2.0.dylib:
	@rpath/libz3.4.15.dylib (compatibility version 4.15.0, current version 4.15.2)
	/usr/lib/libc++.1.dylib (compatibility version 1.0.0, current version 1900.180.0)
	/usr/lib/libSystem.B.dylib (compatibility version 1.0.0, current version 1351.0.0)

~~This conversation may hint that homebrew is doing some extra hacking beyond the package formula to make it work. cmake --install build doesn't fix the problem caused by the default cmake build result.~~

I figured it out. Homebrew names prebuild binary as bottle. The loading path will be renamed from cmake result to their internal macro and renamed to the actual loader path. See the search result (and also kudos for gpt).

These are all for homebrew's z3, not for the opam-z3. I also don't have a good understanding of installing language packages (e.g., ocaml or python) directly into system package managers. How does nix work?

[arbipher]

I have been thinking about this question for installing language packages, e.g., ocaml-z3, into system package managers, e.g., apt/dpkg (or nix if as I guess). As an OCaml developer, for a long time, I took it for granted that people would use an OCaml library to develop. However, I realize that some Debian packages, including ocaml packages, may be necessary to run system-level software developed by OCaml.

So it sounds more reasonable to have install instructions in cmake. Let me check how other Debian packages pack the OCaml packages, and then make the update. However, this mean the platform installation problems return, and we have to take care of the platform subtlety in cmake script.