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

2015-10-22 Thread Enrico Tassi
On Thu, Oct 22, 2015 at 11:55:45AM +0200, Stéphane Glondu wrote: > I see two possible fixes for Debian: either declare that initial.coq is > arch-independent, or declare that .vo files are arch-dependent. I don't > know if the former is safe, but it would be the most convenient. The > disadvantage

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

2015-10-22 Thread Stéphane Glondu
Le 22/10/2015 13:14, Pierre-Marie Pédrot a écrit : >> Does this behaviour ring a bell to someone? Isn't it the symptom of a >> bug somewhere? > > Looks like a bug. Coq object files are arch-dependent but should not > vary depending on byte- or native-compilation, as far as I understand.

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

2015-10-22 Thread Stéphane Glondu
Le 22/10/2015 13:21, Guillaume Melquiond a écrit : >> By "before", I mean ocaml 4.01.0 and camlp5 6.11. By "now", I mean ocaml >> 4.02.3 and camlp5 6.14. In both situations, coq is version 8.4pl4. > > I am using the debian jessie package on amd64 (so 8.4pl4dfsg-1) and I > cannot reproduce your

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

2015-10-22 Thread Pierre-Marie Pédrot
On 22/10/2015 11:55, Stéphane Glondu wrote: > Does this behaviour ring a bell to someone? Isn't it the symptom of a > bug somewhere? Looks like a bug. Coq object files are arch-dependent but should not vary depending on byte- or native-compilation, as far as I understand. I am currently looking

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

2015-10-22 Thread Pierre-Marie Pédrot
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:

Bytecode/native interoperability of .vo/.coq files

2015-10-22 Thread Stéphane Glondu
Hello, I am debugging why why and aac-tactics fail to build on bytecode architectures in Debian with the new OCaml version. I have noticed that generated .vo files differ, depending on whether the file is compiled with the native or the bytecode version of coqtop. This was not the case before.

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

2015-10-22 Thread Gabriel Scherer
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