使用opam安装Z3的ocaml API [英] Installing ocaml API for Z3 using opam

问题描述

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

I want to use Z3 in my OCaml program. Using opam, I did

$ opam install z3
$ eval $(opam env)

然后尝试使用

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

我得到的是从

开始的数千个In function foo undefined reference to bar的巨大转储.

What I get is a huge dump of thousands of In function foo undefined reference to bar, starting with

/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，

What am I doing wrong? For the record, I was using ocamlbuild, with

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

文件中的

和true: package(z3).但是像上面那样调用普通ocamlfind会得到相同的输出.

and true: package(z3) in the _tags file. But calling plain ocamlfind like above gives the same output.

版本:编译器:带有flambda的4.06.1，opam:2.0.0，z3:4.8.4.

Versions: compiler: 4.06.1 w/ flambda, opam: 2.0.0, z3: 4.8.4.

推荐答案

TL; DR;包裹坏了.以下是修复程序和一些变通办法，但通常，此类问题应发布到相应的问题跟踪器.因此，请考虑打开问题报告或提出带有修复的请求.

TL;DR; The package is broken. The fix and a couple of workarounds are below, but in general, such questions should be posted to corresponding issue trackers. So consider opening an issue report or pull request with a fix.

这些链接器错误表明C ++标准库中的符号丢失.由于OCaml使用C链接器链接最终产品，因此默认情况下不会传递C ++标准库.当然，正确制作的软件包应该为我们 ¹ 做到这一点，但是我们仍然可以通过-cclib -lstdc++手动进行此操作(如果您具有libstdc ++，则使用-lc++).

Those linker errors indicate that the symbols from the C++ standard library are missing. Since OCaml is using the C linker to link the final product it is not passing the C++ standard library by default. Of course, a properly made package should do this for us¹, but we can still do it manually via the -cclib -lstdc++ (if you have libstdc++, otherwise use -lc++).

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

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

With ocamlbuild you can use the cclib(x) parametrized tag, e.g.,

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

给沙丘用户的笔记

TL; DR;如果您使用的是dune，则仍然必须在库/可执行节中添加(flags (-cclib -lstdc++))，因为沙丘会忽略linkopts(以及META文件的许多其他字段).

A note for the dune users

TL;DR; If you're using dune then you still have to add (flags (-cclib -lstdc++)) to your library/executable stanza, since dune is ignoring linkopts (and many other fields of the META files).

长话短说. META文件规范由findlib库定义和实现.沙丘构建系统未使用findlib，而是重新实现了findlib的一小部分，其中缺少许多功能，例如linkopts和谓词等字段.因此，尽管事实是META规定了此字段，但仍需要添加此字段.至少截至2019年10月.

Long story. The META file specification is defined and implemented by the findlib library. The dune building system is not using findlib, instead they have re-implemented a small subset of findlib with many features missing, namely fields like linkopts and predicates. That's why you still need to add this field, despite the fact, that META prescribes it. At least as of October 2019.

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

¹ the provided META file contains a bogus

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

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

which (a) doesn't make sense since -L is not a linker option, but the compiler one, and (b) is useless, as /usr/lib is usually in the search path anyway.

正确的选项应该是:

linkopts = "-cclib -lstdc++"

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

You might edit the file directly, it is located at $(ocamlfind query z3)/META.

请考虑提交对OPAM软件包或(理想情况下)对z3的修复程序.

Please, consider submitting a fix either to OPAM package or (ideally) to z3.

这篇关于使用opam安装Z3的ocaml API的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！