The Coq mailing list

[Yannick Forster <yannick AT yforster.de>]

> Or are you saying that the -Q and -R options have these two distinct
> purpose?  In which case, I suppose you say
> coqc -Q ... xx genT.v
> (but what goes in the place of the ...)

If you are in the same directory as genT.v

coqc -Q . xx genT.v

should work (i.e. the relative path "." which says "this directory").

Usually the first line of _CoqProject files does something equivalent, e.g.

-Q . Undecidability

here: 
https://github.com/uds-psl/coq-library-undecidability/blob/coq-8.12/theories/_CoqProject#L1

>  and if you need to use say
> coqc -Q XX xx -Q YY yy genT.v
> does the file genT.vo contain library xx.genT or yy.genT?

It depends on XX and YY.

For

coqc -Q . MyProject -Q ../lib Library genT.v

genT.vo should be MyProject.genT.


On 20/01/2021 13:13, Jeremy Dawson wrote:
> On 20/1/21 7:27 pm, Guillaume Melquiond wrote:
> > 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
>
> Thanks but I understood that the -Q and -R options control where Coq 
> looks to find compiled .vo files.  This is what I understand from
>
> "-Q directory dirpath
>
>      Add physical path directory to the list of directories where Coq 
> looks for a file and bind it to the logical directory dirpath."
>
> and
>
> "The command line option -R is a variant of -Q which has the strictly 
> same behavior regarding loadpaths, but which also makes the 
> corresponding .vo files available ..."
>
> and
>
> " Command Add LoadPath string as dirpath
>      dirpath
>      ::=
>      ident .* ident
>
>      This command is equivalent to the command line option -Q string 
> dirpath"
> (and I know from using it that Add LoadPath tells Coq where to look for 
> compiled .vo files).
>
> The question is about how to compile a file genT.v in a way that it 
> provides library xx.genT rather than library genT, not about how to tell 
> it where to look for files which it Imports.
>
> Or are you saying that the -Q and -R options have these two distinct 
> purpose?  In which case, I suppose you say
> coqc -Q ... xx genT.v
> (but what goes in the place of the ...)
> and if you need to use say
> coqc -Q XX xx -Q YY yy genT.v
> does the file genT.vo contain library xx.genT or yy.genT?
>
> Thanks
>
> Jeremy