[Date Prev][Date Next] [Thread Prev][Thread Next] [Date Index] [Thread Index]

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



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

Attachment: signature.asc
Description: OpenPGP digital signature


Reply to: