The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

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