Le 08/03/2018 à 13:53, Abhishek Kumar a écrit :
I have 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 Why3 API with regular OCaml code?
You have to point your compiler to the directory where the API is
installed. The exact directory depends on whether ocamlfind was used.
The configure script should tell you so.
If ocamlfind was not used, the following command should work:
ocamlc -I +why3 foo.ml
If ocamlfind was used, the following command should work:
ocamlfind ocamlc -package why3 foo.ml
If neither of them work, then
ocamlc -I /whatever/the/configure/script/said foo.ml
Best regards,
Guillaume
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
