The Coq mailing list

[Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>]

Sorry, I don't understand what you are getting at.  What do you mean by
make *and make install* tense-logic-in-Coq
ie what do I type and in what directory?
What is "make install" meant to do?

Thanks

Jeremy


On 4/28/20 12:01 AM, Pierre Courtieu wrote:
> 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 
> <mailto: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