Bytecode/native interoperability of .vo/.coq files

[Stéphane Glondu <steph@glondu.net>]

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.

More precisely, the attached file compiled with "coqc -nois" and "coqc
-byte -nois" produces two distinct files now, whereas it used to produce
identical files before.

Does this behaviour ring a bell to someone? Isn't it the symptom of a
bug somewhere?

As a consequence, the digest for the same library compiled with the
native or the bytecode version of coqtop changes. It seems still
possible to load a natively-compiled library into a bytecode coqtop,
though. Is that safe? Same remark/question with initial.coq.

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 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 of the latter being it would force the compilation of
"pure" Coq libraries on all architectures (and coq-float and mathcomp
are particularly long to compile). But doesn't the new native vmcompute
of 8.5 force compilation of pure Coq libraries everywhere anyway?


Cheers,

-- 
Stéphane

Reserved Notation "{ x }" (at level 0, x at level 99).

(** Notations for sigma-types or subsets *)

Reserved Notation "{ x  |  P }" (at level 0, x at level 99).
Reserved Notation "{ x  |  P  & Q }" (at level 0, x at level 99).