Установка ocaml API для Z3 с помощью opam

Question

Я хочу использовать Z3 в моей программе OCaml.Используя опам, я сделал

$ 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 с 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++)

---

¹ предоставленный файл META содержит фальшивку

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

, который (a) не имеет смысла, поскольку -L не является компоновщиком, а компилятором, а (b) бесполезен, так как /usr/lib обычно в любом случае находится в пути поиска.

Правильный вариант должен быть:

linkopts = "-cclib -lstdc++"

Вы можете редактировать файл напрямую, он расположен в $(ocamlfind query z3)/META.

Пожалуйста, рассмотрите возможность отправки исправления в пакет OPAM или (в идеале) в z3.