The Coq mailing list

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

Le 20/01/2021 à 03:13, Jeremy Dawson a écrit :

> when I was trying to use CoqProject with all the suggestions various
> people made.  Would that be correct?  Is "xx" here, or the absence of
> it, a "logical name"?  And how does one compile a Coq file (genT.v) to
> make it contain the library xx.genT rather than the library genT?
> And (I know I must sound like a broken record here, but I'm just as sick
> of it as anyone reading it) is this anywhere in the documentation?

Yes it is.

https://coq.inria.fr/distrib/current/refman/language/core/modules.html#libraries-and-filesystem
https://coq.inria.fr/distrib/current/refman/proof-engine/vernacular-commands.html#loadpath

For short, Coq uses a virtual filesystem to locate .vo files. Paths to
files from the (potentially numerous) physical filesystems of your
computer are mapped into this single virtual filesystem (where they get
"logical" paths). If you want file /foo/bar/genT.vo to be assigned the
logical path xx.genT, you need to add the following lines to your
_CoqProject file:

  -R /foo/bar xx

Remarks:

1. You can also use -Q instead of -R. See the documentation for the
difference between those two.

2. You can (and often should) use physical paths relative to the
directory of your _CoqProject file, instead of absolute ones.

3. If you invoke coqc directly rather than through the Makefile
generated by coq_makefile, you need to pass the exact same -R/-Q option
as above on its command line. (You might have to adjust the physical
paths if you are using relative ones, depending on which directory you
are running coqc from.)

4. For installed libraries, Coq takes care of automatically adding the
corresponding -R/-Q options, e.g.,

  -R /path/to/coq/theories Coq
  -Q /path/to/coq/user-contrib/xx xx
  -Q /path/to/coq/user-contrib/yy yy

So, you do not need to mention already installed libraries in your
_CoqProject file.

5. ``Add Rec LoadPath "/foo/bar" as xx.'' is equivalent to using the -R
option. ``Add LoadPath "/foo/bar" as xx.'' is equivalent to using the -Q
option.

Best regards,

Guillaume