The Coq mailing list

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

Hi Pierre,

Thanks.  I'm not sure what "library" means in the Coq context (and it's 
not in the documentation index).  Locate Library seems to work for a 
single filename (without the v) but I'm guessing that's not what you mean.

Anyway, there are 3 directories containing Coq source files, called
lnt/tense-logic-in-Coq, gen and modal

The one I'm most commonly making changes in, and whose Coq files depend 
on the other two, is modal.

Can the _CoqProject file mechanism can handle this situation?  It sounds 
from what you say that it can't.

Where you say the Int directory I assume you mean lnt but going there 
and typing make does nothing because it does not contain a makefile.

In lnt/tense-logic-in-Coq there is a Makefile but it was not produced by 
coq_makefile.  It works nicely for compiling all the Coq files in that 
directory.  It doesn't have a target "install"

Likewise the directory gen does not have a makefile (yet).

Cheers,

Jeremy


On 28/4/20 1:31 am, Pierre Courtieu wrote:
> I suppose that Int, gen, and the current directory are actually 3 
> different coq libraries. If this is not the case you need to tell us a 
> bit more. If this is the case then they should not share the same 
> _CoqProject file.
>
> 1) Go inside Int directory and type make, if it went well, then do "make 
> install".
> 3) do the same in directory gen
>
> now coq knows about Int and gen without any -Q option. Write your 
> _CoqProject by mentioning only your files. By default "make install" 
> copies .vo files into <coq_directory>/user-contrib/<libdirectoryname>, 
> which is searched by coq by default.
>
> Hope this helps,
> Pierre
>
> Le lun. 27 avr. 2020 à 16:50, Jeremy Dawson <Jeremy.Dawson AT anu.edu.au 
> <mailto:Jeremy.Dawson AT anu.edu.au>> a écrit :
>
>     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>
>      > 
> <mailto: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
>      >