The Coq mailing list

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

Hi,

thanks, I did this.  Now I get a myriad of warnings, of which I show the 
last,

*** Warning: in file modal/k4.v,
    required library gstep matches several files in path
    (found gstep.v in gen and gen/ib; used the latter)
COQC lnt/tense-logic-in-Coq/gen.v
COQC lnt/tense-logic-in-Coq/existsT.v
COQC lnt/tense-logic-in-Coq/genT.v
COQC lnt/tense-logic-in-Coq/ddT.v
COQC lnt/tense-logic-in-Coq/dd_fc.v
COQC gen/rtcT.v
File "./gen/rtcT.v", line 9, characters 0-41:
Warning: Cannot open ../lnt/tense-logic-in-Coq [cannot-open-path,filesystem]
transitiveT
     : forall W : Type, relationT W -> Type
make[1]: *** No rule to make target 'gen/ib/gstep.vo', needed by 
'gen/gentree.vo'.  Stop.
make: *** [Makefile:318: all] Error 2

There's nothing about gen/ib in the _CoqProject file.

Is this error because of using -R instead of -Q?

Cheers,

Jeremy

On 29/4/20 12:11 am, Jason Gross wrote:
> Run `make clean` before `make` to remove all the outdated .vo files that 
> you previously produced with different settings, which are incompatible 
> with the new ones.
>
> On Tue, Apr 28, 2020, 10:03 Jeremy Dawson <Jeremy.Dawson AT anu.edu.au 
> <mailto:Jeremy.Dawson AT anu.edu.au>> wrote:
>
>     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
>      >>