While trying to make Why3 plugins also work in bytecode mode, I am encountering some difficulties:
$ cat foo.ml
let () = Dynlink.loadfile_private ".../why3/plugins/microc.cma"
$ ocamlfind ocamlc -package why3 -linkpkg -linkall foo.ml && ./a.out
Fatal error: exception Dynlink error: error while linking .../why3/plugins/microc.cma.
Reference to undefined global `Mc_parser'
The thing is, Mc_parser
is the very first unit in microc.cma
, so I am confused as to why Dynlink complains about it being undefined.
$ ocamlobjinfo .../why3/plugins/microc.cma | head
File .../why3/plugins/microc.cma
Force custom: no
Extra C object files:
Extra C options:
Extra dynamically-loaded libraries:
Unit name: Mc_parser
Interfaces imported:
30d209d6ccecb36afd436e1096ff74c1 Why3
49c6c492a189deeaed5bf77a6793e7fa Unix
6ae0781ff0acd08a308bc4a9842d91d9 Str
Using ocamlopt
instead of ocamlc
makes the code succeed. Using Dynlink.loadfile
instead of Dynlink.loadfile_private
also makes the code succeed. (This can be reproduced with a plain installation of Why3 obtained with opam install why3
.)
Is Dynlink.loadfile_private
broken in bytecode mode or is there something else going on?