The Coq mailing list

[Christoph-Simon Senjak <christoph.senjak AT ifi.lmu.de>]

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

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

Or did I get that wrong? Any other clues?

Best regards
Christoph-Simon Senjak