The Coq mailing list

[Christian Doczkal <christian.doczkal AT inria.fr>]

I think the use of "library" in the Coq context is slightly ambiguous.
It can refer to a single file (as with Locate Library) or to a
collection of (compiled) files sharing a common namespace. I say
compiled here, because the namespace is fixed during compilation.

Libraries that are set up to be used by others usually fix a namespace
identifier in their Makefile and the install target then installs the
library (i.e., all the compiled files) to ../coq-contrib/<namespace>.
From there they can be used via "From <namespace> Require Import <lib>.

In the context where you are touching files from several libraries
(folders in this context) and you're not installing anything globally,
the setup you describe is fine. (I actually used a setup similar to what
you describe, simply ignoring the warnings)

However, it may be cleaner to use a centralized build infrastructure
residing in the shared top-level directory. You could try starting with
a _CoqProject file containing someting along the lines of

INSTALLDEFAULTROOT = mylib #silence no common root warning
-R/-Q lnt/tense-logic-in-Coq
-R/-Q gen
-R/-Q modal

plus the output of

$ ls -1 lnt/tense-logic-in-Coq/*.v gen/*.v modal/*.v

One advantage is that this allows make to track dependencies across the
various folders and compile (in parallel) only what is necessary.

(coq_makefile -h also lists an "-install none" option, but the generated
Makefile in my tests still had an install target on coq-8.11.1 ...)

Best,
Christian


On 4/28/20 8:08 AM, Jeremy Dawson wrote:
> 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
>>      >
>>