coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>
- To: Pierre Courtieu <pierre.courtieu AT gmail.com>, Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] how to require file in subdirectory
- Date: Fri, 7 Feb 2020 13:20:12 +0000
- Accept-language: en-US
- Arc-authentication-results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=anu.edu.au; dmarc=pass action=none header.from=anu.edu.au; dkim=pass header.d=anu.edu.au; arc=none
- Arc-message-signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=yhm41fF/jYSGIeNpEyZ+hWWnEf17f6jMjViBnHhPMGc=; b=fcPl7r2A1wCLzgd5Xdi3Ui+PJkWF7y4Vry8hY9MKeV/wqJzkPFfKcASg0AL6tiTzoFrbXk+fU4o4tDzcP3EzViZ0HEqkeuKYsvshC0cQx4aI25ZWrzt8HV79Necbf5YGhyQE+vzPpA6nT0oPaZdzoVzQ9GhTOd4r+5PqIANy+ZGVYAvAXa6/PYccDCZmOOB7Rf6vKaJtxjh0YNApNnuFOWlud133Bx+N1tdoRUctzpptytnra2F0lBGTI2hGzG5LnL1oezQI3SSAv48y8eymcvb3clO+SBSPdSeyF7QAWlH9kP8fQd+nNJsMvximvITjIYj2eyLdq21KJw6h037hsg==
- Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=n1EcZKU7wASNg72cwL10gowmOryY6gnlymF8LLb8G4UiEe7Grvyw+LB7nF7+dJJHzwqEb6h9t3efhGTRwk3dwwBMDe7eSvkNugU6t7QVx9q5FLsaIntSUm4P8CzuF6tG35Xco774bEwrg9CAZegCrgsemL/aQfkXUs5AR5Piva9Za3XUm8U4wHodnMLKhkYtCYLgfhIuk3TeaFHP4RdnxibjDFxZRE5duDNPIoOvHcKR+uhcR5K/XZwiZ1bsF+0ccP8bOxnMXqAk+/rFE3yWxD0A4xehOhzykZOhm1g8i9IqZTpdsUSjf2zQaYFLGo/rKlmz1mk/Gv608fHHo3GF4g==
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.mailfrom=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.helo=postmaster AT AUS01-ME1-obe.outbound.protection.outlook.com
- Ironport-phdr: 9a23:BqKc+h9XjWqdCv9uRHKM819IXTAuvvDOBiVQ1KB+0+gWIJqq85mqBkHD//Il1AaPAdyHra8ZwLaH++C4ACpcuM3H6ChDOLV3FDY9wf0MmAIhBMPXQWbaF9XNKxIAIcJZSVV+9Gu6O0UGUOz3ZlnVv2HgpWVKQka3OgV6PPn6FZDPhMqrye+y54fTYwJVjzahfL9+Nhq7oRjeu8UMgYZvKqk9xxTNr3BVf+ha2X5kKUickhrh6Mq85oJv/zhVt/k868NOTKL2crgiQ7dFFjomKWc15MPqtRnHUwSC42YXX3sVnBRVHQXL9Qn2UZjtvCT0sOp9wzSaMtbtTb8oQzSi7rxkRwHuhSwaKjM26mDXish3jKJGvBKsogF0zoDIbI2JMvd1Y7jQds0GS2VfQslRVjRBAoKiYIsJE+oBJvtTo43kq1cTsReyGQygCeXywTFKm3D2x7U33eQ/Hw/bwAwuEdEAsHrWo9X0KKgcXu+6wbLUzTrYdf5axSvx5JTKfx0nvPqCXahwcc3UyUQ3Ew3KkE+QppLgPzKVy+8DvXKU7uR7VeKojW4stgZ8rDyxycc2lIbJg4IUxkrK+ypjzoc1Ptq4SEhgbNG+FptQqjuWOJVrTcM/WW1nojs6x6QAtJWmciYKz5EnyATea/yBa4WI5wrjVOeILTdjinNlY6izhxGo8Uiv0uH8V8+00ExLriVfiNXMuGoN2wTc6siGVvt9/lqh1i2V2w/P7eFEJEY5nrfYJZ452rM9mYYfvV7eEiPqmkj6lrKae0sl9+Sy9ujrfLrrqoeTOoJwkA3yL6Ajl8ylDegmMQUCRXaX9fm92bDl4Eb3Wq9FjucsnancqJ3aJdoUpqq+AwJNzoss5QuxAyu73NgBmncJI09JdAuAj4fyJV7COvf4Deqjg1u3lzdr2vbGMaD7DpXVNHjDl6vhcqhh5E5AyQozytZf64hTCrEcPPLzXkjxtNvbDhMjLwO0xOPnBM181oMYR22PHreUPazOvVOS++4jP+uBaJUItDvzKvUp/ePigWE2lFMFeKmmx5oXaHS2HvR8JEWZZGLhjNMfHmcQoAU+SezrhEeMXzFJaXeyRKU85jcgBY28C4fDW5qhj6Kc0yemBJFZfH1GBkiWEXj0b4WER+sMaCWKL8B9lTwETKGtRJMl1RGzrwD30KFnL+rR+i0Ar53vztl15+vJlREz7zN4Fcqd03veB11zy1sJSiUs0ehUplFn1laOzOAsm/1VD8ZeofhOTx0mNJPB5+N/AtH2HAnGe4HNAH2hW52NBSw7BoY6xMZLaEJgEf2jiArC1mykGelGuaaMAckW/7jR2mm5C89i0HHAnP0DgkMrR9oJGWS5nal53wHVGsjEn1jfnrv8JvdU5zLE6GrWlTnGh0pfSgMlFPydBSlDNHuTlszw4wb5d5HrEa4ua1ETwMifbKZGd5vgkAceHaqxCJHle2u03lyIK1OIy7eLMNW4UlgmhHyYLWVd1gcZ8DCBKBQ0ATqnryTGFjtyGFnzYkTqt+5jtHe8SUxyxAaPPRQ4huiFvyUNjPnZcMs9m7cNuSMvsTJxRQzv1tTLTdeMukxoYfcFbA==
thanks Pierre - I'd found one of these but not the other
Jeremy
On 2/7/20 1:26 AM, Pierre Courtieu wrote:
> FTR this is documented in the "PRACTICAL TOOLS/ Coq Command" chapter of the
> documentation:
>
> https://coq.inria.fr/distrib/current/refman/practical-tools/coq-commands.html
>
> and in "PRACTICAL TOOLS/ Utilities":
>
> https://coq.inria.fr/distrib/current/refman/practical-tools/utilities.html#utilities
>
> P.
>
> Le jeu. 6 févr. 2020 à 15:23, Ralf Jung
> <jung AT mpi-sws.org>
> a écrit :
>>
>> Hi Jeremy,
>>
>> if it helps to see an example, you can check out how we are using
>> _CoqProject in
>> Iris:
>>
>> https://gitlab.mpi-sws.org/iris/iris/blob/master/_CoqProject
>>
>> In particular, note the "-Q theories iris". This means that the folder
>> "theories" (relative to the _CoqProject file) becomes the Coq logical path
>> "iris".
>>
>> With this, you can just open any .v file in theories/* in CoqIDE, and all
>> the
>> paths just work. No need to pass any flags anywhere else. (Well, this is
>> what
>> happens with ProofGeneral, but I think CoqIDE is the same.) And as already
>> mentioned in this thread, the coq_makefile invocation is
>>
>> coq_makefile -f _CoqProject -o Makefile
>>
>> After that, running "make" will build all files listed in _CoqProject.
>> (Notice that if you have a typo in that file list, really weird stuff can
>> happen
>> -- that's a known bug: https://github.com/coq/coq/issues/9319.)
>>
>> Kind regards,
>> Ralf
>>
>> On 06.02.20 15:09, Jeremy Dawson wrote:
>>> Hi Theo,
>>>
>>> Thanks. How about coqide (it's been mentioned to me previously, but
>>> apparently it has the same options as coqtop, and it's documentation
>>> within the reference manual doesn't seem to mention the _CoqProject file).
>>>
>>> And so far, I'm pretty much on my own regarding this _CoqProject file -
>>> I can't find any documentation about how to set it up, when it is used,
>>> and what it does. Is there any such documentation?
>>>
>>> Thanks for the tip about echo $?
>>>
>>> Jeremy Dawson
>>>
>>>
>>> On 6/2/20 7:48 pm, Théo Zimmermann wrote:
>>>> Hi Jeremy,
>>>>
>>>> The _CoqProject file is supported by editors with Coq support (Emacs
>>>> with PG, VsCode with VsCoq, etc.) and by coq_makefile. You are never
>>>> supposed to run coqc nor coqtop directly by yourself. In particular,
>>>> today coqtop is considered as just a debugging tool. If you do insist on
>>>> using it standalone, you are pretty much on your own (and you'll have to
>>>> figure out the flags you need to give it).
>>>>
>>>> Regarding how to make sure that a process such as make finished without
>>>> error, you can print the exit code: echo $?
>>>>
>>>> Cheers,
>>>> Théo
>>>>
>>>>
>>>> Le jeu. 6 févr. 2020 à 01:59, Jeremy Dawson
>>>> <Jeremy.Dawson AT anu.edu.au
>>>> <mailto:Jeremy.Dawson AT anu.edu.au>>
>>>> a écrit :
>>>>
>>>> Well, make with the existing Makefile seems to make everything OK, I
>>>> suppose there is no way to tell for sure, but there is no apparent
>>>> error.
>>>>
>>>> With a new _CoqProject file there are all sorts of errors,
>>>> presumably
>>>> because the existing _CoqProject file has useful stuff in it.
>>>>
>>>> But in any event, running coq (to be exact, coqtop) does not access
>>>> either _CoqProject or Makefile, so I can't see how your solution
>>>> should
>>>> work. (Anyway, it doesn't). Maybe I'm missing something here. Can
>>>> you
>>>> explain how your solution should work.
>>>>
>>>> Or can anyone refer me to where the documentation on this issue is,
>>>> if any?
>>>>
>>>> Thanks
>>>>
>>>> Jeremy
>>>>
>>>>
>>>> On 5/2/20 7:59 pm, Donald Leung wrote:
>>>> > Dear Jeremy,
>>>> >
>>>> > Try adding a `_CoqProject` file in the root directory of your Coq
>>>> development with the following contents:
>>>> >
>>>> > ```
>>>> > -Q ./tttt/TTT/ tttt.TTT
>>>> >
>>>> > ./tttt/TTT/ssss.v
>>>> > ./tttt/TTT/file2.v
>>>> > ./tttt/TTT/file3.v
>>>> > …
>>>> > ./tttt/TTT/filen.v
>>>> > ```
>>>> >
>>>> > where file2.v, file3.v, …, filen.v are the other vernacular files
>>>> in your Coq development that you would also like to compile. Then
>>>> run:
>>>> >
>>>> > ```bash
>>>> > $ coq_makefile -f _CoqProject -o Makefile
>>>> > ```
>>>> >
>>>> > in your command line and select `Compile > Make` in your CoqIDE
>>>> (or similar). Provided the build is successful, you should then be
>>>> able to step through the line:
>>>> >
>>>> > ```coq
>>>> > From tttt.TTT Require Import ssss.
>>>> > ```
>>>> >
>>>> > in your CoqIDE (or similar) without any issues.
>>>> >
>>>> > Yours sincerely,
>>>> > Donald
>>>> >
>>>> >> Jeremy Dawson
>>>> <Jeremy.Dawson AT anu.edu.au
>>>>
>>>> <mailto:Jeremy.Dawson AT anu.edu.au>>於2020年2月5日
>>>> 15:00寫道:
>>>> >>
>>>> >> Hi,
>>>> >>
>>>> >> I'm trying to run a command which I was guessing should be
>>>> >>
>>>> >> From tttt.TTT Require Import ssss.
>>>> >>
>>>> >> but I get the error
>>>> >>
>>>> >> Cannot find a physical path bound to logical path matching
>>>> suffix
>>>> >> <> and prefix tttt.TTT.
>>>> >>
>>>> >> What does this mean?
>>>> >>
>>>> >> How do I use a file tttt/TTT/ssss.vo?
>>>> >>
>>>> >>
>>>> >> The documentation contains
>>>> >> Variant From dirpath Require qualid
>>>> >> (in
>>>> >>
>>>>
>>>> https://coq.inria.fr/distrib/current/refman/proof-engine/vernacular-commands.html#coq:cmdv.from-require)
>>>> >>
>>>> >> What should a dirpath look like, and where is it to be found in
>>>> the
>>>> >> documentation? (Some of these syntax constructs seem to be
>>>> defined in
>>>> >>
>>>>
>>>> https://coq.inria.fr/distrib/current/refman/language/gallina-specification-language.html
>>>> >> but dirpath isn't - and none of them seem to be in the index)
>>>> >>
>>>> >> Thanks
>>>> >>
>>>> >> Jeremy
>>>> >
>>>>
>>
>> --
>> Website: https://people.mpi-sws.org/~jung/
- [Coq-Club] how to require file in subdirectory, Jeremy Dawson, 02/05/2020
- Re: [Coq-Club] how to require file in subdirectory, Donald Leung, 02/05/2020
- Re: [Coq-Club] how to require file in subdirectory, Jeremy Dawson, 02/05/2020
- Re: [Coq-Club] how to require file in subdirectory, Gaëtan Gilbert, 02/05/2020
- Re: [Coq-Club] how to require file in subdirectory, Jeremy Dawson, 02/06/2020
- Re: [Coq-Club] how to require file in subdirectory, Théo Zimmermann, 02/06/2020
- Re: [Coq-Club] how to require file in subdirectory, Jeremy Dawson, 02/06/2020
- Re: [Coq-Club] how to require file in subdirectory, Ralf Jung, 02/06/2020
- Re: [Coq-Club] how to require file in subdirectory, Pierre Courtieu, 02/06/2020
- Re: [Coq-Club] how to require file in subdirectory, Jeremy Dawson, 02/07/2020
- Re: [Coq-Club] how to require file in subdirectory, Pierre Courtieu, 02/06/2020
- Re: [Coq-Club] how to require file in subdirectory, Théo Zimmermann, 02/06/2020
- Re: [Coq-Club] how to require file in subdirectory, Ralf Jung, 02/06/2020
- Re: [Coq-Club] how to require file in subdirectory, Jeremy Dawson, 02/06/2020
- Re: [Coq-Club] how to require file in subdirectory, Théo Zimmermann, 02/06/2020
- Re: [Coq-Club] how to require file in subdirectory, Jeremy Dawson, 02/05/2020
- Re: [Coq-Club] how to require file in subdirectory, Donald Leung, 02/05/2020
Archive powered by MHonArc 2.6.18.