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.