The Coq mailing list

[Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>]

OK, so I've put some random name (corresponding to your a below)
which isn't used, but then, having run coq_makefile and then make I get 
the following

[jeremy@localhost coq]$ coq_makefile -f _CoqProject -o Makefile
[jeremy@localhost coq]$ make
COQC lnt/tense-logic-in-Coq/cut.v
File "./lnt/tense-logic-in-Coq/cut.v", line 3, characters 0-20:
Error:
The file /home/jeremy/coq/lnt/tense-logic-in-Coq/genT.vo contains library
genT and not library xxx.genT

make[1]: *** [Makefile:657: lnt/tense-logic-in-Coq/cut.vo] Error 1
make: *** [Makefile:318: all] Error 2

Jeremy

On 28/4/20 11: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