Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Add LoadPath in Coq 8.12.2

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Add LoadPath in Coq 8.12.2


Chronological Thread 
  • From: Yannick Forster <yannick AT yforster.de>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Add LoadPath in Coq 8.12.2
  • Date: Wed, 20 Jan 2021 14:25:07 +0100
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=yannick AT yforster.de; spf=Pass smtp.mailfrom=yannick AT yforster.de; spf=None smtp.helo=postmaster AT himalia.uberspace.de
  • Ironport-hdrordr: A9a23:22CqN6wJVnWK2v+/weF+KrPxxeskLtp033Aq2lEZdDV+dMuEm8ey2NES0hHpgDgcMUtQ/uyoEq+GXH/a6NpJ+oEXJ7ivR03Lv2GvIYFk4+LZslvdMgf58fNQ0rolTrhmBLTLfDxHpOvz/QXQKbYd6fad9qTAv4vj5ldrCTpncqRxqzp+Yzzrd3FeYCljKd4HGIGH5sxBzgDQG0g/SsigHHEKU6ziirTw9a7OWhINCx455ATmt1rBg9THOiOV0RsEXzREza1Kywb4ujbk7aauuezT8HLh/lLUhq44pPLc0NdZQOSDhs8JQw+c6TqVTYFqbb2OrVkJieuo70snl8SJph8mMdh65X+5RBDTnTLm3Q783DEyr2L4wViDjnf55cD/TjQ2C81O7LgpFCfx4Uwmod16zeZXz3uU3qAnaS/okSzh67HzNy1CmVGzpRMZ/dI7j3saSocGba8UsIp3xjIxLL4FEDjh4I4qVOliZfu82N9TcVeXK2/UpXNuxtvEZAVQIj6cTkIPutOY3lFt9RgTpXcw38ARkmwN85gwUfB/idjsKLhil71FU6YtAJ5VGeFpe6SKI3DWTQmJOGyfJkmPLtBlB07w
  • Ironport-phdr: A9a23:EZky+RXcQVgc7jgJC6IqxQJLHjfV8KyXUjF92vIco4ILSbyq+tHYBGea288FpGHAUYiT0f9Yke2e6/mmBTVRp8/b+y1YONwUDllZ0JpQx1RhSOe+SmTDZMbwaCI7GMkQHHRExFqcdXZvJcDlelfJqWez5zNBUj/2NA5yO/inUtWK15f/2O+94YDcbBtVjzShf7xyMA+2rQLMvcUKnIduMKk8xgbNr3dSZuha22xkKFKNkx3h4su84INv/z5ftv489cNMS7n2c7g9QbdFEDkoLmc56dHxuxLeVwWP/HwcUmsXkhpMHQfI6QzxU4nyvCXnqOdzwTGWMsLqQ786XzSi9LprRwTziCgbLT458XrYhdJ2galGvR+uvR1/w4rTYIGIKPpze77WcN0GSWZdWMtaSipMCZ6+YYQSFeoMJftWoYnjqVsArhWwCwejC+ztxTBUiXH7xrE63uc7HA3awAAtEdADvXLJp9v1LqcSVuW1wbHKwjrZafNW3zb955TLchs8of+MWqhwcdHNyUYxDQPOk1KdqIz/MDOT0OQNsnSU7+l7WOOvhW4nrBtxoiOzxsgykInFnJ8axU7d+Ch/3Y06KsG2RlRhbt64DJtfqTuaN41uT84tXmxltzg3x70btZKmfiUHypopygPdZvGFfIWF7Q7vWPqSLDpkh39pZrayihS9/0Wu1ODyWca63llOoydFnNfBsG0G2RLU6siCUPR9/0Gh1C6A1wDS9uFEIV00mrHBJ5E9xb4wk4IfsETDHyPsl0X5kqmWdlk89uip7eTneLTmqYWGO496kAHzNLkllM+nAekgLwQDXGiW9f6i2LDi50H1XbVHg/wsnqXErpzXJMIWrbOjDQBPyIYs8RO/Ai+m0NsGmXkHK0pIeBKGj4jsIV7OJPH4Au2lj1Sxizhk2erGPqb5AprXMnfMjq3tcqtj5EJEyQozy85Q545MB70cI//+WlX9uMLZAxMjLgC5w+fqBM9g2o8AWG+DGqqZP7nTsV+M6OIvOe6MZIoNtTf9Mfcl4fjujX4lll8eZqSo3ZUXaHeiHvR9P0WWf2Dsjs0cHmgUpgY+VvDliEWeUT5PYHa/R74z5jYiCI6/EYjDQp2tj6ea0SegHpxWY3hGBUqWHXfpcYWEQfYMZziILs9viDxXHYSmHoQmzFSlsBLw47thNOvdvCMC5rz5090g1uTVkxA59nRaCN6Gz2yXBzVll2UORjQ19LFxplZm1lqZl6R11a8LXedP7u9EB19pfaXXyPZ3XoiacjKERc+ATROdevvjGSs4JvogzdgUeFpwAZOug0KbtwKaRoQNnrnOP6Qat6LR23+ZD8Z8zn/C1aBnklMrWNBXPGarwKJypVC7L76MqF2QkuORTYpZ2SfM8GmZym/mlFBWVxRrTajfG3wSNBK+kA==

> 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



Archive powered by MHonArc 2.6.19+.

Top of Page