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: Pierre Courtieu <pierre.courtieu AT gmail.com>
  • To: Coq Club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] _CoqProject
  • Date: Mon, 27 Apr 2020 16:01:42 +0200
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=pierre.courtieu AT gmail.com; spf=Pass smtp.mailfrom=pierre.courtieu AT gmail.com; spf=None smtp.helo=postmaster AT mail-io1-f44.google.com
  • Ironport-phdr: 9a23:zHEFqhfnPohc30OarrYIzW16lGMj4u6mDksu8pMizoh2WeGdxcuybB7h7PlgxGXEQZ/co6odzbaP7ua9CCdesN6oizMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpTEdFQ/iOgVrO+/7BpDdj9it1+C15pbffxhEiCCybL9vLBi6twXcu80ZjYZjLqs61wfErGZPd+lK321jOEidnwz75se+/Z5j9zpftvc8/MNeUqv0Yro1Q6VAADspL2466svrtQLeTQSU/XsTTn8WkhtTDAfb6hzxQ4r8vTH7tup53ymaINH2QLUpUjms86tnVBnlgzocOjUn7G/YlNB/jKNDoBKguRN/xZLUYJqIP/Z6Z6/RYM8WSXZEUstXSidPAJ6zb5EXAuUOM+ZXrYnzqVUNoxWjGwejGPjixSVUinLsx6A2z/gtHAPA0Qc9H9wOqnPUrNDtOakIUOC60rPIzS/dYPhLxzr975XIcgo9ofGNQ71wbNfaxE43FwPEkFqQs5blMC2P2usRtGib8vBgVf6ui2E5tgF8uTevxsI2hYnIgoIZ0EzL9SJ8wIssI9CzVU11Yca8HZdOqy2XM5F6T8AiTm1ypSo3y7wLtYS0cSUFzpks2gTRZOadc4eS5xLuTOaRLil8hHJiYL+/ggy98UmkyuHlV8m010tGojNLktTDuX0BzRPT6s+ASvty+keuxyyD2BzU6uFBOUw0lKzbJIA9wrMoiJYfrUDOEjX1lUj2lqOaa0Qp9+my5+nobbjqvpqcOJV1igH6PKQugMu/AeEgPwgWXmiU5/681Kf98kHjXLpKieA2krPFsJDbO8sbu7W0AwBQ0ok56ha/Cy2q38gfnXkCNF5FYg6Ij5D1O1HSJ/D1Feuwg1O1kDty2//GOqDhDY7WI3jYkLbheK595FRGxAoyy9Bf/ZNUBasbLPL9QE+i/ODfWzQ+KkSfx/vtQIF20ZpbUmaSCIeYNrnTuBmG/LR8DfOLYdotuTvnMfVtzPnzl2M4lEJVKbGo0IENZTazGel8P0SUfFLjh94AFSEBuQ9oH7+is0GLTTMGPyX6ZKk7/DxuTdv+Vd6SFLDou6SI2WKAJrMTY2lHDl6WFnKxLteLXv4NbGSZJcozy2VYB4jkcJco0FSVjCG/06Bud7OG9SgRtJal399wtbWKyEMCsAdsBsHY6FmjCmF5mmRSGm0z1aF75E16kxKNjfQ+jPtfGtheofhOV1ViOA==

Hi

These warnings mean that your current configuration does not allow to do "make install" due to the lack of a main root directory. coq_makefile does not support to install several libraries at once. However I think you should be able to built your project without problems.

That said if you make *and make install* tense-logic-in-Coq you could just remove it completely from you _CoqProject file, use it in your development and have a working "make install".

Hope this helps,
P


Le lun. 27 avr. 2020 à 13:39, Jeremy Dawson <Jeremy.Dawson AT anu.edu.au> a écrit :
Hi,

Thanks - but this won't work because it would mean changing dd_fc.v
and all the files in that directory, which is part of other people's
work as well

So I tried some alternatives like
-Q ../lnt/tense-logic-in-Coq/
or
-Q ../lnt/tense-logic-in-Coq/ .

All of these, including your suggested
-Q ../lnt/tense-logic-in-Coq/ TL

gave a bunch or warnings, eg

-Q ../lnt/tense-logic-in-Coq/ TL
gives
Warning: ../lnt/tense-logic-in-Coq/ (used in -R or -Q) is not a
subdirectory of the current directory

Warning: no common logical root
Warning: in such case INSTALLDEFAULTROOT must be defined
Warning: the install-doc target is going to install files
Warning: in orphan_TL_Top

I don't understand any of these, except the first (and I don't know what
I should do about that), and I can't find any explanation of these in
the documentation.

What do they all mean?

Thanks

Jeremy


On 27/4/20 12:26 am, Gaëtan Gilbert wrote:
> Indeed -I is for ocaml files (for plugins)
>
> Gaëtan Gilbert
>
> On 26/04/2020 16:23, Dan Frumin wrote:
>> Hi Jeremy,
>>
>> I don't know why -I doesn't work, but I think using -Q does the trick
>> (at least with my version of Coq): I replaced
>>
>>      -I ../lnt/tense-logic-in-Coq/
>>
>> with
>>      -Q ../lnt/tense-logic-in-Coq/ TL
>>
>> and then in dd_fc.v used `Require Import TL.genT`
>>
>>
>>
>> Best,
>> Dan
>>
>>
>> On 26-04-2020 16:09, Jeremy Dawson wrote:
>>>
>>> Hi,
>>>
>>> I've constructed a _CoqProject file as follows
>>>
>>> -I ../lnt/tense-logic-in-Coq/
>>> -I ../gen/
>>> ../lnt/tense-logic-in-Coq/gen.v
>>> ../lnt/tense-logic-in-Coq/genT.v
>>> ../lnt/tense-logic-in-Coq/List_lemmasT.v
>>> ../lnt/tense-logic-in-Coq/lntT.v
>>> ../lnt/tense-logic-in-Coq/swappedT.v
>>> ../lnt/tense-logic-in-Coq/ddT.v
>>> ../lnt/tense-logic-in-Coq/dd_fc.v
>>> ../lnt/tense-logic-in-Coq/lntacsT.v
>>> ../gen/rtcT.v
>>> ../gen/gstep.v
>>> ../gen/gentree.v
>>> gen_ext.v
>>> k4.v
>>> k4_exch.v
>>> k4_inv.v
>>> k4_ctr.v
>>> k4_ca.v
>>>
>>> I then run
>>>   make -f Makefile
>>> and get the following messages
>>> COQC ../lnt/tense-logic-in-Coq/dd_fc.v
>>> File "../lnt/tense-logic-in-Coq/dd_fc.v", line 12, characters 15-19:
>>> Error: Unable to locate library genT.
>>>
>>> (in fact the file
>>> ../lnt/tense-logic-in-Coq/genT.v
>>> exists)
>>>
>>> What do I need to put in the _CoqProject file to make this work?
>>>
>>> Thanks
>>>
>>> Jeremy



Archive powered by MHonArc 2.6.18.

Top of Page