WIP: Migrating OCaml binding to CMake

[arbipher]

It's my WIP working on migrating the building of OCaml binding to CMake.

I think the majority of the work is done. I started by mimicking the other bindings and some llvm cmake for ocaml, but then I just manually wrote enough custom commands and dependencies. The actual building commands should have the same result as the previously generated python scripts, though I think I simplified some unnecessary dependencies and compiler flags.

tldr;

  cd build && cmake \
-G "Ninja" \
-DZ3_BUILD_LIBZ3_SHARED=TRUE \
-DZ3_BUILD_OCAML_BINDINGS=TRUE \
-DZ3_USE_LIB_GMP=TRUE \
../

It should just work. I also build and run the ml_examples.ml for both bytecode and native code in the cmake to make sure it works. I observe all z3 bindings are using shared library so I wonder maybe I don't even need to make a static version for the ocaml-binding.

I also add one argument -DZ3_BUILD_OCAML_EXTERNAL_LIBZ3=/path/to/libz3.so to support building ocaml building with an external z3 library that is often installed by some other distro package managers.

Now the remaining work is :

1. The installation part. I really don't have a good idea for non opam installation.
2. Test it on macos. I knew the problem and the two-line fix for macos's problem. It's in the comments yet.
3. Remove unnecessary files.
4. Write some good document for it.
5. Tune for the CI.
6. (this is out of z3 but) Make opam package for this new building script. However, I guess I have to adjust both sides to try letting it work well.

p.s. for ocaml users, I also have a post for discussion.

[arbipher]

Thank you so much for your careful examination. This is one reason I would like to make this immature draft PR. I am learning how z3 is installed on some platforms so my change won't break them. Also, I am still thinking how the ocaml-binding should be installed.

I will check your changes one by one later.

[NikolajBjorner]

It would be absolutely great to cmake-ify the ocaml bindings for uniform build support and allow to retarget release processes to use the more portable cmake system.

[arbipher]

Aha, I was occupied by some random things after the previous effect on this issue in July. I hope to pick this up this month.

[arbipher]

I made some updates (finally) to the PR. After it looks good to you, I can cherry-pick them to the latest commit and make another PR.

For the previous review,

• I removed all the necessary source file copying.
• I deleted AddOCaml.make, which was used for llvm.

I added Github Action and made it work on both ubuntu and macOS. They work (finally finally) on my forked repo.

For the linking especially rpath-related, since platforms like Debian (discourage), homebrew(hacking) or even opam have its own mechanism to handle, in this build I just figured out a way (mainly for macOS) to make two working build and run as sanity check.

The next step is to allow external libz3 and allow binding to be built with them. I am still not very clear on the current Windows support for ocaml as well as the users will use a Windows native binding.

[NikolajBjorner]

Regarding Windows + OCaml: It isn't (was never before) a big use case and nowadays it is very easy to start up wsl2/ubuntu for ocaml development.

I sometimes tease @msprotz on his past heroic efforts in this space, so thanks for the reminder.

[arbipher]

Cool for the merging. There is a debug helper makefile in it (which shouldn't be a big deal and I will remove it in the next PR for the next steps).