The Coq mailing list

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

Hi Christian,

Thanks - I'm not sure what you mean by "the setup you describe is fine" 
because nothing I've described so far has worked.

Anyhow, I've tried your suggestion:  I assume "-R/-Q" means choose 
either "-R" or "-Q" (without assuming this, coq_makefile produces errors).

Then coq_makefile seems to work OK but then "make" produces the following

lots of warnings of which I show the last
*** Warning: in file modal/k4.v, library lntacsT is required and has not 
been found in the loadpath!
COQC lnt/tense-logic-in-Coq/cut_extraction_test.v

Error: Invalid character '-' at beginning of identifier "-Q".

make[1]: *** [Makefile:657: 
lnt/tense-logic-in-Coq/cut_extraction_test.vo] Error 1
make: *** [Makefile:318: all] Error 2

Cheers,

Jeremy



On 28/4/20 7:17 pm, Christian Doczkal wrote:
> 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
> > >       >