CODEWITHSUNDEEP
ocamlz3ocamlbuildocaml-dune
bftang
bftang

Reputation: 1

How to solve linking problem on Z3 in OCaml?

when I suppose to use Z3 lib in OCaml

open Z3

the first line is getting Unbound module Z3, which is not able to solve.

the code is able to run correctly when I add

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

However, the first line #use "topfind";; showing as red, and the type checkings are all disappeared. How can I just using open Z3 with out any error showing?

Upvotes: 0

Views: 70

Answers (1)

Chris
Chris

Reputation: 36536

It sounds as though you're not linking the Z3 library into your program. You either need to modify your dune file (if you're using dune) to specify that you're using this library, or for a simple program, you can easily accomplish this with 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 -package z3 z3test.ml
$ ./a.out
hello world!
$

One more thing

Directives like #use and #require should not be necessary outside of a REPL environment like utop.

Upvotes: 1

Related Questions