coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Vladimir Voevodsky <vladimir AT ias.edu>
- To: Jason Gross <jasongross9 AT gmail.com>
- Cc: Guillaume Melquiond <guillaume.melquiond AT inria.fr>, coq-club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Export/Import
- Date: Wed, 1 Jan 2014 19:29:01 -0500
Do not use the user-contrib files which you have - they are not appropriate for the example.
Simply create files:
1. uuutest.v with
Definition UU:Type.
2. uu0test.v with
Require Export "uuu".
in tmp1/tmp2/
3. pathtest with
Require Export "uu0test.v"
in tmp3/
Then do
coqc tmp2/uuutest
coqc tmp2/uu0test
from tmp1/
Then copy tmp2/uuutest.vo and tmp2/uu0test.vo to user-contrib/tmp1/
Then do
coqc pathtest
from tmp3.
This should reproduce the effect.
V.
On Jan 1, 2014, at 6:14 PM, Jason Gross <jasongross9 AT gmail.com> wrote:
I cannot even get your uu0 file to compile as given. Why are you using quotes around the names? Can you give a self-contained set of files and set of commands to generate your problem?jgross@cagnode17:/tmp$ find user-contrib/ -name "*.v"user-contrib/pathnotations.vuser-contrib/Foundations/Generalities/uu0.vuser-contrib/Foundations/Generalities/uuu.vjgross@cagnode17:/tmp$ cat user-contrib/Foundations/Generalities/uuu.vjgross@cagnode17:/tmp$ cat user-contrib/Foundations/Generalities/uu0.vRequire Export "uuu".jgross@cagnode17:/tmp$ cat user-contrib/pathnotations.vRequire Export "uu0".jgross@cagnode17:/tmp$ coqc user-contrib/Foundations/Generalities/uuu.vjgross@cagnode17:/tmp$ coqc user-contrib/Foundations/Generalities/uu0.vFile "./user-contrib/Foundations/Generalities/uu0.v", line 1, characters 0-21:Error: Can't find file uuu.vo on loadpath-JasonOn Wed, Jan 1, 2014 at 6:02 PM, Vladimir Voevodsky <vladimir AT ias.edu> wrote:
No options at all. The files uuu and uu0 were compiled with the command
coqc Generalities/uuu.v
coqc Generalities/uu0.v
from a copy of Foundations/ outside of user-contrib/ and then copied to /user-contrib/Foundations/Generalities/
Are you sure you did not leave a copy of uuu.vo around somewhere other than in user-contrib/Foundations/Generalities/uuu.vo ?
Also it is important:
a. To have quotes around all file names.
b. To have two layers i.e. Foundations/Generalities/
V.
On Jan 1, 2014, at 5:51 PM, Guillaume Melquiond wrote:
> On 01/01/2014 23:04, Vladimir Voevodsky wrote:
>> I get an error message:
>>
>> File "./pathnotations.v", line 2, characters 0-21:
>> Error: Cannot find library uuu in loadpath
>
> I cannot reproduce this bug. The file in the separate directory compiles just fine and transitively imports uuu. Could you tell us which options you have used to compile the three files? Of particular interest are -I and -R.
>
> Best regards,
>
> Guillaume
- [Coq-Club] Export/Import, Vladimir Voevodsky, 01/01/2014
- Re: [Coq-Club] Export/Import, Guillaume Melquiond, 01/01/2014
- Re: [Coq-Club] Export/Import, Vladimir Voevodsky, 01/02/2014
- Re: [Coq-Club] Export/Import, Jason Gross, 01/02/2014
- Re: [Coq-Club] Export/Import, Vladimir Voevodsky, 01/02/2014
- Re: [Coq-Club] Export/Import, Vladimir Voevodsky, 01/02/2014
- Re: [Coq-Club] Export/Import, Jason Gross, 01/02/2014
- Re: [Coq-Club] Export/Import, Vladimir Voevodsky, 01/02/2014
- Message not available
- Message not available
- Message not available
- Message not available
- Re: [Coq-Club] Export/Import, Jason Gross, 01/02/2014
- Re: [Coq-Club] Export/Import, Jason Gross, 01/02/2014
- Re: [Coq-Club] Export/Import, Vladimir Voevodsky, 01/02/2014
- Re: [Coq-Club] Export/Import, Vladimir Voevodsky, 01/02/2014
- Re: [Coq-Club] Export/Import, Jason Gross, 01/02/2014
- Re: [Coq-Club] Export/Import, Vladimir Voevodsky, 01/02/2014
- Re: [Coq-Club] Export/Import, Guillaume Melquiond, 01/01/2014
Archive powered by MHonArc 2.6.18.