Re: [coqdev] Bytecode/native interoperability of .vo/.coq files

[Stéphane Glondu <steph@glondu.net>]

Le 22/10/2015 13:31, Pierre-Marie Pédrot a écrit :
>> If "native"  compilation of the standard library is disabled in
>> bytecode, it could be that some linking information stored in vo files
>> (i.e. where to find the .cmxs files) differ.
> 
> After crawling through votour, I kind of found the culprit, even though
> I have no idea where this difference comes from.
> 
> In the SYNTAX-EXTENSION entry, there is a Extend.constr_prod_entry_key
> attached to the "P" literal which is shared (if I understand well) in
> bytecode but not in nativecode, resulting in two different marshalling.
> More precisely, the precise object whose sharing differ is the pair of
> an Extend.ETConstr constructor.
> 
> Probably related to an optimization in bytecode or some order-relevant
> stuff...

Good catch! Looking at:

  http://caml.inria.fr/mantis/view.php?id=5779#c10927

(and following comments) this difference in sharing between native and
bytecode is new in OCaml 4.02.0 and known.

So the (seemingly) weird behaviour is explained! Then, I guess
unmarshaling on bytecode something that has been marshaled in native
code should be safe.


Cheers,

-- 
Stéphane