ocaml - 为什么我无法在我的 OCaml 代码中使用 Why3 API？

Question

我下载了Why3 tarball 并使用make 安装，并make install-lib按照Why3 API 文档中的说明进行安装。但是当我这样做时open Why3，ocamlc 和 utop 仍然抱怨unbound module Why3。

有人可以帮我如何使用 OCaml 代码中的 Whye API 吗？

我按照这里给出的说明http://why3.lri.fr/doc/install.html。

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

Answer 1

您需要告诉编译器在哪里查找why3 及其依赖项。假设您在 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

或者，如果您有 ocamlfind，则更容易（我建议您使用或更好地使用支持 ocamlfind 的构建系统）。

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