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 issue. Both generated files are identical (and the > md5 is 40b7180...).
This is because you are in the "before" situation. As I said, generated files are identical in this case. > Just so that there is no confusion. There is no native vmcompute. There > is vm_compute on one side and native_compute on the other side. > > And yes, native_compute forces compilation of pure Coq library > everywhere. But that is needed only if you want to offer native_compute > everywhere. This is not mandatory. For instance, this is currently > disabled for Windows builds. > > Moreover, only the standard library is built by default with support for > native_compute. User libraries are not. So you could still keep > coq-float and mathcomp arch-independent if you wished to. OK, thanks for the clarification. > By the way, does Debian support having a package marked as both > arch-independent and arch-dependent? [...] No. > [...] That way, you would provide a > native_compute version for amd64 and a generic version for all the other > architectures. Hmm... I guess you could have two packages > coq-theories-amd64 and coq-theories-generic that are mutually exclusive > and both provide coq-theories. Yes, but I'd rather avoid that. Cheers, -- Stéphane