z3
z3 copied to clipboard
WIP: Migrating OCaml binding to CMake
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 :
- The installation part. I really don't have a good idea for non opam installation.
- Test it on macos. I knew the problem and the two-line fix for macos's problem. It's in the comments yet.
- Remove unnecessary files.
- Write some good document for it.
- Tune for the CI.
- (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.