我正在尝试在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
的方法?
ocamlbuild
的调用是不正确的,上面的那个几乎是正确的,如果你正在使用正确的 CoqMETA
文件,你确实应该只使用-package coq.lib
。 - ejgallego_tags
文件。 - ejgallegoMETA
文件。 - Li-yao Xiaocamlbuild
如何依赖于META
?在_tags
中应该放什么,考虑到需要thread
的部分是我正在使用的库,而不是我的实际代码?一个答案是展示构建上述片段的好方法。 - Li-yao Xia