Error when loading hypothesis_selection.cmxs: undefined symbol: camlGraph
When ocamlfind
builds the hypothesis_selection
plugin, it marks it as depending on graph.cmxs
. Since Why3 itself does not use this shared library, it does not dynamically load it. The bug only occurs if ocamlfind
is used to build Why3 and ocamlgraph
was built as a shared library (e.g., Opam).
So, Why3's Makefile
needs to be modified to statically link graph.cmxa
into hypothesis_selection.cmxs
(when using ocamlfind
). When fixing the bug, be careful not to inadvertently link the other .cmxa
files, especially not why3.cmxa
.
This is a blocker only if we actually care about this plugin.