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.ped...@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 > >
