Re: [coqdev] Bytecode/native interoperability of .vo/.coq files
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 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?
The status quo is that the stdlib is compiled with native-compute on, so
we have .cmxs along with .vo files. But the flag is by default off
when compiling files outside the stdlib. So, while coq-theories will
become arch:any, user contributions can stay arch:all.
Best,
--
Enrico Tassi
Reply to: