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

[Gabriel Scherer <gabriel.scherer@gmail.com>]

Note that, since OCaml 4.01, OCaml marshalling flags include a Compat_32 flag. If set, any marshalling operation involving an integer that cannot be represented on 32-bit OCaml versions will fail at runtime. If you would like to have consistent marshalling behaviour between architectures, enabling it in Coq is probably a good step forward.

(Un-marshalling a 64 bit integer that cannot be represented on 32 from a 32 bit machine always fails. What Compat_32 brings is a failure at marshalling time, from the 64 bit machine.)

On Thu, Oct 22, 2015 at 1:58 PM, Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> wrote:

On 22/10/2015 13:49, Stéphane Glondu wrote:
> Arch-dependent? Really? What is arch-dependent it them?

The representation of integers. Some integers can overflow in 32-bits,
and have a different value in 32-bits and 64-bits. There was a funny bug
in the OCaml marshaler based on that idea:

http://caml.inria.fr/mantis/view.php?id=5793

Most notably hashes differ. Note that we should tend to enforce that all
of our data structures fit on 32-bit integers, but this is a difficult
task, both tedious and error-prone for little profit.

PMP