z3 OCaml bindings - toplevel

1
votes

I've built z3 as described here using the ml-ng branch. Everything seems to have completed fine, except when I want to use z3 in the OCaml toplevel (I try to use the FindLib #require command to import what's needed) I get this error:

Error: The external function `n_is_null' is not available

any ideas on what this is, and how I would go about successfully using z3 in the toplevel?

1
ocamlz3
those 2 links are actually identical. Also, which version did you use? If that's not a actual release, perhaps you should expect things to break. - didierc
Tplevel ocaml is not supported yet. This requires that we add dynamically loadable stubs, which all the version of ocaml on all the platforms I have, refuse to build... so this ones going to take a while. - Christoph Wintersteiger
Thanks for the response @ChristophWintersteiger I'll make do with what works for the moment then. - Ahmad Rasekh
Thanks @didierc, I've fixed the links, I'm using OCaml version 4.02.1, but I guess it makes no difference for now if, as Christoph has said, toplevel isn't supported yet. - Ahmad Rasekh

1 Answers

0
votes

I have just updated the ml-ng branch with a new set of build rules that should build and install a package that also works in the ocaml toplevel. See also the following discussion on codeplex: OCaml bindings status and compilation