Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] _CoqProject

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] _CoqProject


Chronological Thread 
  • From: Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] _CoqProject
  • Date: Wed, 29 Apr 2020 00:30:12 +1000
  • Arc-authentication-results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=anu.edu.au; dmarc=pass action=none header.from=anu.edu.au; dkim=pass header.d=anu.edu.au; arc=none
  • Arc-message-signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=jiom/1fIgAUVxH+lr7T1z1Y+WpnljlSV5fqFGdYJQCs=; b=np3z1/4Ob0qE9A1gNavcQ7yep3J2/0mqIHIPH9vgPTuw/E4x7tLXWnKnxCjy3grS7Q360RZCkxXdcE399DiYJsLHxuKNu/b/BuTCUNdtCKrutLLPVXDwXct33pURnQWIenRaHI4SYT6iX7azBJ7fRZSFGbA6bS/58e1DJrEPcnjwlP+73yPCIQHGlAcVWpvyfrHV7nkaC2NYnQlidt+BCD97qedcI6fWiTG5s33jVxG4hVZQooW8Gr+ROkw5rCI7FL28iO+8PuQiHJuZrgDifJedqgOzpiduEgTWxFyRyycGut20W6c2g3xMgVdQMEnGhKtH3b8j3RQ63xYO4E8PQA==
  • Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=W4nHSJ0DSYWWXSBWGkzvToGNv58BYhRy9m0LjjMHc3nx6WWR8WGEbwulJi/EMKU4Dsj7R4roKeUWQWKhvxhZwpN37d5kJuxrqzbNNrX2lhmPXWb7aK9laIc58YnKU+BYLm11RUDbZiGve1pJmCX+pBf0+S3/HCrvL4YErdwKoE255p9dXUY/wFR5D6M6+rmsidjQr4lGhtxpJdj5eUcZK0nLj4cyHfojTbPuJiWNOKAjIMPWXYFhc7UJAQPtyJagF9xdXLjejNJAEVzmRs9nO/36WHR65CIZIlu+ML+Pl928xWAxyTZdLVvtVdJD/ggigdkit/Oouod7CGI9qb+57g==
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.mailfrom=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.helo=postmaster AT AUS01-SY3-obe.outbound.protection.outlook.com
  • Ironport-phdr: 9a23:O07yPha9El6DHz3ivQlbQLP/LSx+4OfEezUN459isYplN5qZr8m7bnLW6fgltlLVR4KTs6sC17OL9f65EjNdqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba5yIRmsrAjdq8YajIliJ60s1hbHv3xEdvhMy2h1P1yThRH85smx/J5n7Stdvu8q+tBDX6vnYak2VKRUAzs6PW874s3rrgTDQhCU5nQASGUWkwFHDBbD4RrnQ5r+qCr6tu562CmHIc37SK0/VDq+46t3ThLjlSEKPCM7/m7KkMx9lL9VrgyvpxJ/wIDabo+aO/hica3SctwaRHFMXtpSWiFbHo+wc4UCAugHMO1Fr4f9vVwOrR6mCAeoGuzv0CFHhnr23KYn3eouCw/H3BcnH9IIrX/Zq9H7O7kIUe+ryanJzS/PYf1M1jbz84jIdRYhrOqWUrJ2bMrd01cgGB7YjlmKs4PlIiqY2+IQuGaV6OpgUPigi28hqwxpuDeg3N0ghZPTiY0P0lzL7j52z50vKd25VkF2Z8OvHphItyyCOIZ6XtkuT3x0tCs40LEKpJC2cSoQxJg62hLTduSLfoeM7x75SeqcIit0iGhndb+xnRq+7FasxvH6W8KpylhFtDBFncPJtn0V1xzc9MyHSvxl80q91zmByhzf5vxdLU4pl6XWJYctwrkrmZUNq0jDGTL2mFntg6+Ra0Uk/PWn5/7/YrX8oZ+cK5F7hR3iMqQvncy/B/40Mg8TX2iH/eS807rj/U7jTLpWif02l7HVsJHcJcsFuq60GwBY3po55xqiEzur0s4UkWQJIV9HYh6LkpXlN0zWLPD9F/i/glCskDlxx/DBO73sGpHDIWbZkLj/eLZ861RQxgQpwtFR/JJUDbcBLenpVU/3qdzUFAE2PBGpw+r9Etp9y5sSWXiTDa+BLKPSrViI6/ozLOmLfY8ZoSryK/w45/H1lnI5gl8cfayx3ZQNcny4H/JmI1+YYXX2mNsBH30K7UICS7nhj0THWjpObV6zWbg973c1EtGIF4DGE6KgmrGEzW+XF4JNYWYOXnKBC3rtZsOoUugXbyS6K8l81DEISP6oVtlyhlmVqAbmxu8/faLv8SoCuMe7jYQn16jojRg3sAdMIYGFyWjUFTN9mH5OSjMrmqli8xQkmwWzlJNgivkdLuR9ovZAUwM0L5nZlrYoAtbvHA/NY5GAVQT/G4j0MXQKVts0huQ2TQN9FtGl0k+R9heRW+ZQrI3QQZs+/+TbwmT7INt7xzDezq49glI6Q8xJc2q7mqp48AuVDInMwRyU

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




Archive powered by MHonArc 2.6.18.

Top of Page