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

Question

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

我刚刚按照https://github.com/polazarus/z3-installer 的说明成功编译了 Z3 的 OCaml 绑定。他们使用旧的 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: cannot 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's Z3 overlay。他解释了如何编译 Z3。