OCamlbuild链接库的顺序错误。

Question

我正在尝试在OCaml中使用Coq库中的_CoqProject_解析器（如果该库不适用于外部使用，我欢迎更好的替代方案来获取Coq项目的.v文件），但_ocamlbuild_似乎将库链接顺序弄错了。

考虑这个最小化的示例文件。

open CoqProject_file
let x = read_project_file

< p > coq.lib 包（与coq捆绑在一起）某种程度上依赖于threads，并且根据此答案建议使用-tag thread，但是在链接coq.lib时仍会出现以下错误，指出找不到threads：

$ ocamlbuild -pkg coq.lib -tag thread -cflag -rectypes a.native                                                                                                             /tmp/p
+ /home/sam/.opam/4.06.0+coq-8.7/bin/ocamlopt.opt -I /home/sam/.opam/4.06.0+coq-8.7/lib/coq/config -I /home/sam/.opam/4.06.0+coq-8.7/lib/coq/lib -I /home/sam/.opam/4.06.0+coq-8.7/lib/ocaml /home/sam/.opam/4.06.0+coq-8.7/lib/ocaml/str.cmxa /home/sam/.opam/4.06.0+coq-8.7/lib/ocaml/unix.cmxa /home/sam/.opam/4.06.0+coq-8.7/lib/coq/lib/clib.cmxa -thread threads.cmxa a.cmx -o a.native
File "_none_", line 1:
Error: No implementations provided for the following modules:
         Thread referenced from /home/sam/.opam/4.06.0+coq-8.7/lib/coq/lib/clib.cmxa(Exninfo)
         Mutex referenced from /home/sam/.opam/4.06.0+coq-8.7/lib/coq/lib/clib.cmxa(Exninfo)
Command exited with code 2.

如果我将 ocamlopt 的调用拆开并在 clib.cmxa 之前加上 -thread threads.cmxa，那么它就可以编译通过。

$ cd _build/
$ /home/sam/.opam/4.06.0+coq-8.7/bin/ocamlopt.opt -I /home/sam/.opam/4.06.0+coq-8.7/lib/coq/config -I /home/sam/.opam/4.06.0+coq-8.7/lib/coq/lib -I /home/sam/.opam/4.06.0+coq-8.7/lib/ocaml /home/sam/.opam/4.06.0+coq-8.7/lib/ocaml/str.cmxa /home/sam/.opam/4.06.0+coq-8.7/lib/ocaml/unix.cmxa -thread threads.cmxa /home/sam/.opam/4.06.0+coq-8.7/lib/coq/lib/clib.cmxa a.cmx -o a.native

什么是正确的调用ocamlbuild的方法？

- Li-yao Xia

---

ocamlbuild -use-ocamlfind -pkg coq.lib -cflag -rectypes -tag thread a.native 这个命令不知怎么就能工作了，但我真的不知道发生了什么，也许这只是纯粹的运气。所以在将其作为答案之前，我会等待一下。 - Li-yao Xia

事实上，你第一次使用 ocamlbuild 的调用是不正确的，上面的那个几乎是正确的，如果你正在使用正确的 Coq META 文件，你确实应该只使用 -package coq.lib。 - ejgallego

无论如何，你都不应该这样工作，而应该使用一个 _tags 文件。 - ejgallego

谢谢你的建议！我之前不知道有META文件。 - Li-yao Xia

我对正确的设置感到困惑。ocamlbuild 如何依赖于 META？在 _tags 中应该放什么，考虑到需要 thread 的部分是我正在使用的库，而不是我的实际代码？一个答案是展示构建上述片段的好方法。 - Li-yao Xia

Answer 1

如果您使用ocamlfind包，则应使用-use-ocamlfind标志。

关于为什么需要-tag thread标记，目前还没有一个好的解决方案¹。OCaml线程接口有两个不同的实现（一个是os线程，另一个是green线程），而coq.lib依赖于该接口，但不会为用户决定使用哪个接口，因此您必须手动指定，例如使用-tag thread。

¹：一个解决方案是通过废弃vmthreads（green线程，实际上很少使用）来消除这种选择。

- gasche