The Coq mailing list

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

Hello.

On 18.08.2015 07:41, Guillaume Melquiond wrote:
> 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?

There is only an interp/coqlib.ml, which does not contain a variable 
coqlib. config/coq_config.ml exists, and sais

> let coqlib = Some "/usr/local/lib/coq"

I cloned from https://github.com/maximedenes/native-coq.git, commit 
7f6f7379b76c9c6240ab8083960a6531efa301c8 (which is the current one).

> > (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
Christoph-Simon Senjak