[Caml-list] Loading of dynamic code works with older OCaml versions, but fails with recent versions (>= 4.02.0)

[Mohamed Iguernlala <iguer.auto@gmail.com>]

Hello,

I'm facing an issue[1] with OCaml versions >= 4.02.0 when
building/using dynamically loaded plugins for/with Alt-Ergo. I
think this is probably due to module aliases. In fact, I'm able
to install and use Alt-Ergo + satML-plugin on OCaml 4.01.0, but
not on OCaml 4.02.0 (or higher).

$ opam sw 4.01.0
$ eval `opam config env`
$ opam remove alt-ergo satML-plugin
$ opam install alt-ergo satML-plugin
$ echo "goal g: 1 + 1 = 2" > foo.why
$ alt-ergo -sat-plugin satML-plugin.cmxs foo.why
File "foo.why", line 1, characters 9-18:Valid (0.0000) (0 steps)

$ opam sw 4.02.0
$ eval `opam config env`
$ opam remove alt-ergo satML-plugin
$ opam install alt-ergo satML-plugin
$ echo "goal g: 1 + 1 = 2" > foo.why
$ alt-ergo -sat-plugin satML-plugin.cmxs foo.why
...
 >> Failure message: implementation mismatch on Options

Is this a known issue (or is it an issue) ? I know that if I
build the binary and the plugin from the same compiled files,
things work well. I was wondering if there is a better solution
that allows to build things separately.

Regards,

Mohamed.

[1] https://github.com/OCamlPro/alt-ergo/issues/22


-- 
Mohamed IGUERNLALA
Senior R&D Engineer, OCamlPro SAS
Research Associate, VALS team, LRI
Webpage: http://www.iguer.xyz
LinkedIn: https://fr.linkedin.com/in/mohamed-iguernlala-71515979