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
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.
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
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
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:
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.
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
7 matches
Mail list logo