coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] _CoqProject, Jeremy Dawson, 04/26/2020
- Re: [Coq-Club] _CoqProject, Dan Frumin, 04/26/2020
- Re: [Coq-Club] _CoqProject, Gaëtan Gilbert, 04/26/2020
- Re: [Coq-Club] _CoqProject, Jeremy Dawson, 04/27/2020
- Re: [Coq-Club] _CoqProject, Pierre Courtieu, 04/27/2020
- Re: [Coq-Club] _CoqProject, Jeremy Dawson, 04/27/2020
- Re: [Coq-Club] _CoqProject, Pierre Courtieu, 04/27/2020
- Re: [Coq-Club] _CoqProject, Jeremy Dawson, 04/28/2020
- Re: [Coq-Club] _CoqProject, Christian Doczkal, 04/28/2020
- Re: [Coq-Club] _CoqProject, Benoît Viguier, 04/28/2020
- Re: [Coq-Club] _CoqProject, Gaëtan Gilbert, 04/28/2020
- Re: [Coq-Club] _CoqProject, Benoît Viguier, 04/28/2020
- Re: [Coq-Club] _CoqProject, Pierre Courtieu, 04/27/2020
- Re: [Coq-Club] _CoqProject, Pierre Courtieu, 04/28/2020
- Re: [Coq-Club] _CoqProject, Jeremy Dawson, 04/28/2020
- Re: [Coq-Club] _CoqProject, Christian Doczkal, 04/28/2020
- Re: [Coq-Club] _CoqProject, Jeremy Dawson, 04/27/2020
- Re: [Coq-Club] _CoqProject, Pierre Courtieu, 04/27/2020
- Re: [Coq-Club] _CoqProject, Jeremy Dawson, 04/27/2020
- Re: [Coq-Club] _CoqProject, Gaëtan Gilbert, 04/26/2020
- Re: [Coq-Club] _CoqProject, Dan Frumin, 04/26/2020
Archive powered by MHonArc 2.6.18.