Re: [coqdev] Bytecode/native interoperability of .vo/.coq files
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
Reply to: