The Coq mailing list

[Benoît Viguier <beviguier AT gmail.com>]

I thought this was not working. I double checked and I guess I missed it
when I was trying the different combinations in the past. Thank you for
bringing that one out. I will update my small script.

-- 
Kind regards,

Benoît Viguier
Software Engineer - PhD Student | Cryptography & Formal Methods
Radboud University | Mercator 1, Toernooiveld 212
6525 EC Nijmegen, the Netherlands | www.viguier.nl

On 4/28/20 11:32 AM, Gaëtan Gilbert wrote:
>
> >      echo "-Q $D YOURLIB.$D" | sed 's/\//./2'>> _CoqProject
>
> Why not do just one "-Q . YOURLIB" instead of one per subdirectory?
>
> Gaëtan Gilbert
>
> On 28/04/2020 11:25, Benoît Viguier wrote:
>> Hi all,
>>
>> Probably not the only way to solve the "problem" but this may be of
>> interest to some Coq users.
>> I wrote the following shell script to generate my _CoqProject:
>>
>> #!/bin/sh
>>
>> # remove _CoqProject if it already exists
>> [ -e _CoqProject ] && rm _CoqProject
>>
>> # generate the path for coqide and coqv
>> for D in $(find * -maxdepth 1 -type d); do
>>      echo "-Q $D YOURLIB.$D" | sed 's/\//./2'>> _CoqProject
>> done
>>
>> echo "" >> _CoqProject
>>
>> # generate the list of files for coq_makefile
>> find * -name "*.v" -print >> _CoqProject
>>
>> coq_makefile INSTALLDEFAULTROOT = YOURLIB -f _CoqProject -o Makefile
>>
>> So far it has been working flawlessly.
>>
>> Kind Regards.
>>
>> -- 
>> Benoît Viguier
>> Software Engineer - PhD Student | Cryptography & Formal Methods
>> Radboud University | Mercator 1, Toernooiveld 212
>> 6525 EC Nijmegen, the Netherlands |www.viguier.nl
>>
>> On 4/28/20 11:17 AM, 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
>>>>>       >
>>>>>