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).