The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

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