OCaml绑定Z3:在OCaml解释器中成功，但在OCaml编译器中失败

Question

我在OCaml解释器和OCaml编译器之间遇到了一些问题。有谁可以帮我？非常感谢!

我刚刚成功地编译了Z3的Z3绑定，并遵循了https://github.com/polazarus/z3-installer的说明。他们使用了一个旧的Z3版本: 4.1

首先，更改文件Makefile.ocaml：

# Findlib package installation obtion, for instance -destdir /usr/lib/ocaml
OCAMLFIND_INSTALL_FLAGS = -destdir /home/maidinh/.opam/4.01.0/lib/

然后，我编译它：

sudo apt-get install camlidl
sudo make
sudo make install

我不知道为什么在没有“sudo”许可的情况下运行“make”时会失败：

• 当我运行'sudo make‘：http://pastebin.com/rhdAMJKf时的终端日志
• 当我只运行'make‘：http://pastebin.com/qvhysRum时，日志上写着"ld: Can find -lcamlidl“(有人能给我解释一下这个问题吗？)

最后，通过运行OCaml解释器4.01.0来测试Z3的OCaml绑定：

./ocaml
#use "topfind";;
#require "z3";;
open Z3;;
Z3.mk_context;;
- : (string * string) list -> Z3.context = <fun>

成功！

但是，我的程序未能使用OCaml编译器运行。这是我的节目：

let _ = print_endline "Start" in
let _ = Z3.mk_context [] in 
()

然后，我编译并运行：

ocamlfind ocamlc -linkpkg -package z3 -c main.ml -o main.cmo
ocamlfind ocamlc -linkpkg -package z3 -o main  main.cmo
./main
Start
Error: internal error

有人能给我解释一下错误吗？非常感谢!

Answer 1

简而言之，Z3 4.1的ML绑定是错误的。在z3-installer的存储库中，我将其还原为4.0。汇编：

ocamlfind remove z3
opam install camlidl
git clone https://github.com/polazarus/z3-installer.git # fresh clean install
cd z3-installer
make
sudo make lib-install
make ocaml-install

请注意，API略有不同，您的示例应该是：

let _ = print_endline "Start" in
let _ = Z3.mk_context_x [||] in 
()

要安装和编译带有ML绑定的新Z3，您应该了解一下Drup的Z3覆盖。他解释了如何编译Z3。