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
