问为什么我无法在我的OCaml代码中使用Why3接口？
EN

Stack Overflow用户

提问于 2018-03-08 16:21:56

回答 1查看 106关注 0票数 0

我下载了Why3压缩包，并按照Why3应用编程接口文档中的说明，使用make和make install-lib进行安装。但是，当我使用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

发布于 2018-03-08 21:44:52

您需要告诉编译器在哪里查找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

票数 1

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/49168479

复制

相似问题

问为什么我无法在我的OCaml代码中使用Why3接口？EN