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
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 cul
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://c
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.
Arch-depe
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 iss
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
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 a
7 matches
Mail list logo