如何解决 Ocaml 中 Z3 的链接问题？

Question

当我想在 Ocaml 中使用 Z3 lib 时

open Z3

第一行得到未绑定模块Z3，无法解决。

当我添加时代码能够正确运行

#use "topfind";;
#require "z3";;
open Z3

但是，第一行

#use "topfind";;

显示为红色，并且类型检查全部消失。 我怎样才能只使用

open Z3

而不显示任何错误？

Answer 1

听起来好像您没有将 Z3 库“链接”到您的程序中。您需要修改您的沙丘文件以指定您正在使用此库，或者对于简单的程序，您可以使用 ocamlfind 轻松完成此操作。

$ cat z3test.ml
open Z3

let () = print_endline "hello world!"
$ ocamlc z3test.ml
File "z3test.ml", line 1, characters 5-7:
1 | open Z3
         ^
Error: Unbound module Z3
$ ocamlfind ocamlc -packafe z3 z3test.ml
$ ocamlfind ocamlc -package zarith ztest.ml
File "z3test.ml", line 1:
Error: Module `Z3' is unavailable (required by `Z3test')
$ ocamlfind ocamlc -package z3 z3.cma z3test.ml
$ ./a.out
hello world!
$