使用 opam 为 Z3 安装 ocaml API

Question

我想在我的 OCaml 程序中使用 Z3。使用 opam，我做到了

$ opam install z3
$ eval $(opam env)

然后尝试编译

$ ocamlfind ocamlopt -o main -package z3 -linkpkg main.ml

我得到的是数千个In function foo undefined reference to bar 的巨大转储，从

/home/andrepd/.opam/4.06.1+flambda/lib/z3/libz3-static.a(api_datatype.o): In function `mk_datatype_decl':
api_datatype.cpp:(.text+0x4bf): undefined reference to `__cxa_allocate_exception'
api_datatype.cpp:(.text+0x522): undefined reference to `__cxa_throw'
api_datatype.cpp:(.text+0x57b): undefined reference to `__cxa_free_exception'
api_datatype.cpp:(.text+0x58f): undefined reference to `__cxa_allocate_exception'
api_datatype.cpp:(.text+0x5f9): undefined reference to `__cxa_throw'
api_datatype.cpp:(.text+0x61f): undefined reference to `__cxa_allocate_exception'
api_datatype.cpp:(.text+0x68b): undefined reference to `__cxa_throw'
...

结尾

binary_heap_upair_queue.cpp:(.text._ZN2lp23binary_heap_upair_queueIjE7dequeueERjS2_[_ZN2lp23binary_heap_upair_queueIjE7dequeueERjS2_]+0x1ab): undefined reference to `__cxa_allocate_exception'
binary_heap_upair_queue.cpp:(.text._ZN2lp23binary_heap_upair_queueIjE7dequeueERjS2_[_ZN2lp23binary_heap_upair_queueIjE7dequeueERjS2_]+0x205): undefined reference to `__cxa_throw'
binary_heap_upair_queue.cpp:(.text._ZN2lp23binary_heap_upair_queueIjE7dequeueERjS2_[_ZN2lp23binary_heap_upair_queueIjE7dequeueERjS2_]+0x226): undefined reference to `__cxa_free_exception'
/home/andrepd/.opam/4.06.1+flambda/lib/z3/libz3-static.a(binary_heap_upair_queue.o): In function `_GLOBAL__sub_I_binary_heap_upair_queue.cpp':
binary_heap_upair_queue.cpp:(.text.startup+0xc): undefined reference to `std::ios_base::Init::Init()'
binary_heap_upair_queue.cpp:(.text.startup+0x13): undefined reference to `std::ios_base::Init::~Init()'
collect2: error: ld returned 1 exit status
File "caml_startup", line 1:
Error: Error during linking
Command exited with code 2.

我做错了什么？作为记录，我使用的是 ocamlbuild，与

$ ocamlbuild -use-ocamlfind -cflag '-linkpkg' main.native

和true: package(z3) 在_tags 文件中。但是像上面那样调用普通的 ocamlfind 会给出相同的输出。

版本：编译器：4.06.1 w/flambda，opam：2.0.0，z3：4.8.4。

Answer 1

TL;DR;包裹坏了。修复和一些解决方法如下，但一般来说，此类问题应发布到相应的问题跟踪器。因此，请考虑打开问题报告或请求修复。

这些链接器错误表明缺少 C++ 标准库中的符号。由于 OCaml 使用 C 链接器来链接最终产品，因此默认情况下它不会通过 C++ 标准库。当然，正确制作的包应该为我们执行此操作¹，但我们仍然可以通过 -cclib -lstdc++ 手动执行此操作（如果您有 libstdc++，否则使用 -lc++）。

ocamlfind ocamlopt -linkpkg -cclib -lstdc++ -package z3 example.ml -o exe

使用ocamlbuild，您可以使用cclib(x) 参数化标签，例如，

 <example.ml>: cclib(-lstdc++)

沙丘用户须知

TL;DR;如果您使用的是dune，那么您仍然需要将(flags (-cclib -lstdc++)) 添加到您的库/可执行节中，因为dune 忽略了linkopts（以及META 文件的许多其他字段）。

说来话长。 META 文件规范由 findlib 库定义和实现。沙丘构建系统没有使用 findlib，而是重新实现了 findlib 的一小部分，其中缺少许多功能，即 linkopts 和谓词等字段。这就是为什么你仍然需要添加这个字段，尽管 META 规定了它。至少截至 2019 年 10 月。

---

¹ 提供的 META 文件包含伪造的

linkopts = "-cclib -L/usr/lib"

其中 (a) 没有意义，因为 -L 不是链接器选项，而是编译器选项，并且 (b) 没用，因为 /usr/lib 通常无论如何都在搜索路径中。

正确的选项应该是：

linkopts = "-cclib -lstdc++"

您可以直接编辑文件，它位于$(ocamlfind query z3)/META。

请考虑向 OPAM 包或（理想情况下）向 z3 提交修复。