coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Benoît Viguier <beviguier AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] _CoqProject
- Date: Tue, 28 Apr 2020 13:59:20 +0200
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=beviguier AT gmail.com; spf=Pass smtp.mailfrom=beviguier AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm1-f43.google.com
- Ironport-phdr: 9a23:1V2SdxHSEQXxseLxNl5xl51GYnF86YWxBRYc798ds5kLTJ78oM2wAkXT6L1XgUPTWs2DsrQY0reQ7fmrBTBIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfLN/IA+3oAnMucUbjoRvIbstxxXUpXdFZ/5Yzn5yK1KJmBb86Maw/Jp9/ClVpvks6c1OX7jkcqohVbBXAygoPG4z5M3wqBnMVhCP6WcGUmUXiRVHHQ7I5wznU5jrsyv6su192DSGPcDzULs5Vyiu47ttRRT1jioMKjw3/3zNisFokaxVvhyhqRx8zYDabo6aO/hxcb/Sc94BWWpMXdxcWzBdDo6ybYYCCfcKM+ZCr4n6olsDtQazCheqBOPoxCdImmf50qI70+QuDAHG3RIvH8gTu3nTt9r6KrkSUeG6zKnVzDXMcelW1Czy6IjNaB8hoPWMUahsfsrWzEkiDgXIhUiep4ziOjOazOUNs26D4up+VOKvhHMnqwBvrTi13MssjI3Ji4QIwV7H7SV02Jg5KcG8RUJhYtOpEIFcuzyEO4Z1WM8vTG9ltD44x7AEo5K3YSoHxIo9yxLDcfCLbZWE7xLlWe2MOzl3nmhld6i6hxuq8Uiv1On8Vs6s3VZPtCVFk93MumkD1hzW98SLU/V980iv1DqV2ADT7eZEIU8wlaXFMZIu3rkwlp8LvUTCGC/5hln2gbeIekk4/uWk8efqb7X8qpOBKYN5iRvyP6sgl8CnBOQ3KAkOX2yV+eSm073j+FX0T65Ugf0ok6nZv43aJcUFqa6jGAJV3YMj5Ay+DzeiytgXgX4HLFdddBKdk4fpI03OIOz/Dfqnn1usly5ry+naMb3lH5XCNWPOkKzhfLZ4805T0hA/zdFZ55JOC7EOOuj/WkHrtI+QMhhsOAuthu3jFd9V14UEWGvJDLXKHrnVtAqi6+QopfW7Wo4apTfwMbBx7fPwjHAkmFIHVaas1JoTLnu/G6I1cA2ifXPwj4JZQi8xtQ0kQbmy0QHQYXtof3+3GpkEyHQjEov/VNXMQ4mshPqK2yLpRsQHNFADMUiFFDLTT6vBXv4NbCyIJco4y24LULGgT8kq0hT87VanmYoiFfLd/2gjjbym1NVx4LeOxxQ79DgxEMHElm/RFCd7mWQHQzJw16d68xRw
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
>>>>> >
>>>>>
- Re: [Coq-Club] _CoqProject, (continued)
- Re: [Coq-Club] _CoqProject, Dan Frumin, 04/26/2020
- Re: [Coq-Club] _CoqProject, Gaëtan Gilbert, 04/26/2020
- Re: [Coq-Club] _CoqProject, Jeremy Dawson, 04/27/2020
- Re: [Coq-Club] _CoqProject, Pierre Courtieu, 04/27/2020
- Re: [Coq-Club] _CoqProject, Jeremy Dawson, 04/27/2020
- Re: [Coq-Club] _CoqProject, Pierre Courtieu, 04/27/2020
- Re: [Coq-Club] _CoqProject, Jeremy Dawson, 04/28/2020
- Re: [Coq-Club] _CoqProject, Christian Doczkal, 04/28/2020
- Re: [Coq-Club] _CoqProject, Benoît Viguier, 04/28/2020
- Re: [Coq-Club] _CoqProject, Gaëtan Gilbert, 04/28/2020
- Re: [Coq-Club] _CoqProject, Benoît Viguier, 04/28/2020
- Re: [Coq-Club] _CoqProject, Pierre Courtieu, 04/27/2020
- Re: [Coq-Club] _CoqProject, Pierre Courtieu, 04/28/2020
- Re: [Coq-Club] _CoqProject, Jeremy Dawson, 04/28/2020
- Re: [Coq-Club] _CoqProject, Christian Doczkal, 04/28/2020
- Re: [Coq-Club] _CoqProject, Gaëtan Gilbert, 04/28/2020
- Re: [Coq-Club] _CoqProject, Jeremy Dawson, 04/28/2020
- Re: [Coq-Club] _CoqProject, Jason Gross, 04/28/2020
- Re: [Coq-Club] _CoqProject, Jeremy Dawson, 04/28/2020
- Re: [Coq-Club] _CoqProject, Jeremy Dawson, 04/27/2020
- Re: [Coq-Club] _CoqProject, Pierre Courtieu, 04/27/2020
- Re: [Coq-Club] _CoqProject, Christian Doczkal, 04/28/2020
- Re: [Coq-Club] _CoqProject, Jeremy Dawson, 04/27/2020
- Re: [Coq-Club] _CoqProject, Jeremy Dawson, 04/28/2020
- Re: [Coq-Club] _CoqProject, Gaëtan Gilbert, 04/28/2020
- Re: [Coq-Club] _CoqProject, Gaëtan Gilbert, 04/26/2020
- Re: [Coq-Club] _CoqProject, Dan Frumin, 04/26/2020
Archive powered by MHonArc 2.6.18.