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

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

[Mohamed Iguernlala]

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

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

[François Bobot]

Le 31/07/2017 à 18:37, Mohamed Iguernlala a écrit :
> 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.

Alt-Ergo is using pack, so in which way is it linked with 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).

Is satML-plugin compiled by looking only at Alt-Ergo packed library?

Best,

-- 
François

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

[Fabrice Le Fessant]

[-- Attachment #1: Type: text/plain, Size: 1119 bytes --]

We found the reason: it looks like strings are included in the computation
of cmx hashes after 4.02, but not before. Removing a string containing the
time of build will probably solve the issue.
--Fabrice

On Tue, Aug 1, 2017 at 11:16 AM François Bobot <francois.bobot@cea.fr>
wrote:

> Le 31/07/2017 à 18:37, Mohamed Iguernlala a écrit :
> > 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.
>
> Alt-Ergo is using pack, so in which way is it linked with 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).
>
> Is satML-plugin compiled by looking only at Alt-Ergo packed library?
>
> Best,
>
> --
> François
>
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa.inria.fr/sympa/arc/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>

[-- Attachment #2: Type: text/html, Size: 1732 bytes --]