The Coq mailing list

[Christian Doczkal <christian.doczkal AT inria.fr>]

Thank you for clarifying the difference between -Q and -R.

So, if I understand right, if one has a single directory project that is
built using  "-R theories <prefix>" and then installed using the
standard install target, other users still need to use "From" or fully
qualified names. Put differently, there is no observable difference once
the library is compiled/installed, right?

I assume that within said theories folder, local libraries take
precedence over Coq.* libraries that are also available unqualified.
Correct? (The documentation doesn't seem to specify this)

If so, the main source of confusion for library development using -R
would be to inadvertently shadow or unshadow something from the standard
library, while the benefit would be not having to mention the install
prefix within the library.

Best,
Christian


On 4/28/20 3:39 PM, Gaëtan Gilbert wrote:
> If you have files
> 
> A/AA/AAA.v
> B/BB/BBB.v
> 
> and use flags -R A a -Q B b, the following work:
> 
> Require AAA.
> Require AA.AAA.
> Require a.AA.AAA.
> From a Require AAA.
> From a Require AA.AAA.
> Require b.BB.BBB.
> From b Require BBB.
> From b Require BB.BBB.
> 
> ie with -Q you must use either From or the full name, with -R you don't
> have to (which can be fragile when mixing developments).
> 
> coq_makefile installs in user-contrib, and each directory D in
> user-contrib is treated as though you had -Q /path/to/user-contrib/D D
> 
> Gaëtan Gilbert
> 
> On 28/04/2020 15:26, Christian Doczkal wrote:
>> Hi
>>
>>> Anyhow, I've tried your suggestion:  I assume "-R/-Q" means choose
>>> either "-R" or "-Q" (without assuming this, coq_makefile produces
>>> errors).
>>
>> Yes.
>>
>>> Then coq_makefile seems to work OK but then "make" produces the
>>> following
>>>
>>> lots of warnings of which I show the last
>>> *** Warning: in file modal/k4.v, library lntacsT is required and has not
>>> been found in the loadpath!
>>> COQC lnt/tense-logic-in-Coq/cut_extraction_test.v
>>
>> Ah sorry, the syntax of -R and -Q is [-R physicalpath logicalpath] so
>> all three -R/-Q lines need a logical path as well (i.e., the prefix you
>> use in "From <prefix> Require Import <lib>). Something like TL, gen,...)
>>
>> The difference between -R and -Q is IIRC whether the files inside the
>> folder use the prefix when including other files from the same folder or
>> not.
>>
>>> Error: Invalid character '-' at beginning of identifier "-Q".
>>> make[1]: *** [Makefile:657:
>>> lnt/tense-logic-in-Coq/cut_extraction_test.vo] Error 1
>>> make: *** [Makefile:318: all] Error 2
>>
>> make is trying to use -Q as logical path, which obviously fails ...
>>
>> Hope this helps!
>> Christian
>>