z3 icon indicating copy to clipboard operation
z3 copied to clipboard

WIP: Migrating OCaml binding to CMake

Open arbipher opened this issue 8 months ago • 1 comments

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 avatar Jun 17 '24 00:06 arbipher