The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

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> 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
>>