The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

On 17/08/2015 23:04, Christoph-Simon Senjak wrote:
> Hi.
>
> I am trying to use Native-Coq to compile some of my code, and it ...
> sometimes ... works, and sometimes it doesn't, with no apparent reason.
>
> So here is a configuration where it fails:
>
> > $ coqc Shorthand.v
> > File "./NShorthand.ml", line 1, characters 0-17:
> > Error: Unbound module Nativevalues
> > Anomaly: Library compilation failure. Please report.
>
> Using strace, I found out that it executes the following ocamlopt command:
>
> > ocamlopt -shared -o ./NShorthand.cmxs -rectypes -w -A -I
> > /usr/lib/ocaml/camlp5 -I /usr/local/config -I /usr/local/lib -I
> > /usr/local/kernel -I /usr/local/library [...]
> I think
>
> > -I /usr/local/kernel -I /usr/local/library
>
> should be
>
> > -I /usr/local/lib/coq/kernel -I /usr/local/lib/coq/library

Yes. What does your config/coqlib.ml:coqlib variable contains?

> (and probably /usr/local/config also /usr/local/lib/coq/config)

That is surprising. Which version of coq are you using? I am asking 
because your first three -I options should be tempdir, coq/kernel, and 
coq/library. So you have three extraneous -I options and you are missing 
one.

Best regards,

Guillaume