How to use z3 ocaml bindings?

[necto]

Hello, I was searching over the internet how to use ml bindings, and found only entries from the year 2012 and older.
The readme in examples/ml promises that the example will be compiled together, but it does not. After I do

$ python contrib/cmake/bootstrap.py create
$ mkdir build
$ cd build
$ cmake ..
$ make

I found only c, c++ and tptp examples in the build/examples. There is no trace of any OCaml binary.

[necto]

Nevermind. I found the instruction here:
https://z3.codeplex.com/discussions/473552

It says:

$ python scripts/mk_make.py --ml
$ cd build
$ make
$ make examples
$ LD_LIBRARY_PATH=. ./ml_example

[delcypher]

@necto Building the OCaml bindings has not been implemented for the CMake build system yet. I don't have time to do it now but contributions are welcome.

[necto]

Why does Z3 have multiple build systems (CMake, automake configure script, custom python scripts)?
Which one do you plan to support?

[martin-neuhaeusser]

I will try to integrate the OCaml bindings into the CMake build system once I can spare some time. They should work with the custom (python-based) build system.

[delcypher]

@necto The python/Makefile based build sytem (scripts/mk_make.py) is Z3's original build system and the only one that is officially supported. While it is basically functional it has several flaws that really annoyed me so I started implementing a replacement that uses CMake and was first merged in #461. I've been gradually improving it by implementing missing features (e.g. adding support for building the Java bindings).

The CMake build system is not officially supported but I'm hoping it will be accepted as a replacement build system once it reaches feature parity with the old build system. Until that happens we need to have the two build systems exist in parallel with each other.

[NikolajBjorner]

Super, I mostly use the cmake based system and i would assume many others do. Dan did a super job. For Adding missing targets it helps knowing how to operate cmake and also having use of the new target.

[wintersteiger]

@martin-neuhaeusser: Fantastic, thanks for tackling this one! They should indeed work with the current build system, but we recently had a bug report about the bytecode version not working (#724), so something may have changed in OCaml land again.

[NikolajBjorner]

so the status of this is still open and related to #986?

[delcypher]

@NikolajBjorner Yes I've not had time to implement the OCaml bindings for the CMake build system. It's rather a lot of work and there's no benefit for me so I have very little motivation to do the work. I will have some free time in a few months to do this but of course if someone else wants to tackle this I'll happily review the changes.

[NikolajBjorner]

@delcypher, of course. Martin is an ocaml user and expressed intent to do something. The cmake system has so other advantages.

[martin-neuhaeusser]

I will have a look into this - sadly, time has been a rather limited resource :-(
But I agree that having the OCaml bindings in cmake would be nice. I see what I can do.

[delcypher]

@martin-neuhaeusser Have you had a chance to look at implementing the OCaml bindings for CMake? I have a bit of spare time over the next few weeks so I can start implementing this if you haven't already.