Why I am unable to use Why3 API in my OCaml code?

Question

I downloaded the Why3 tarball and installed using make and make install-lib as given in the documentation for Why3 API. But still when I do open Why3, ocamlc and utop complain unbound module Why3.

Can someone please help me how to use Whye API from OCaml code?

I am following instructions give here http://why3.lri.fr/doc/install.html.

./configure
make
sudo make install
make byte opt
make install-lib

Answer 1

You need to tell the compiler where to look for why3 and its dependencies. Assuming you installed everything in DIR:

ocamlc -I DIR/num -I DIR/zip -I DIR/menhirLib -I DIR/why3 \
 unix.cma str.cma dynlink.cma nums.cma zip.cma menhirLib.cmo why3.cma \
 yourfile.ml

Or more easily if you have ocamlfind (I advise you to, or better, use a build system that supports ocamlfind).

ocamlfind ocamlc -package why3 \
 unix.cma str.cma dynlink.cma nums.cma zip.cma menhirLib.cmo why3.cma \
 yourfile.ml