coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jason Gross <jasongross9 AT gmail.com>
- To: Vladimir Voevodsky <vladimir AT ias.edu>, coq-club <coq-club AT inria.fr>, Guillaume Melquiond <guillaume.melquiond AT inria.fr>
- Subject: Re: [Coq-Club] Export/Import
- Date: Thu, 2 Jan 2014 15:10:25 -0500
I have managed to reproduce the bug, and reported it at https://coq.inria.fr/bugs/show_bug.cgi?id=3203.
Vladimir, the PS4 and set -x lines make bash print out the lines that get executed.
-Jason
On Thu, Jan 2, 2014 at 2:37 PM, Vladimir Voevodsky <vladimir AT ias.edu> wrote:
1. You do not have quotes around uu0test in pathtest.2. Do not use -R option in coqc but do cd to tmp1/tmp2/ before compiling.V.PS BTW in the script what are the lines PS4=.. and set -x ?On Jan 2, 2014, at 1:53 PM, Jason Gross wrote:It was not. However, I still cannot get your error message. I can getFile "./pathtest.v", line 1, characters 0-23:Error: The file /afs/csail.mit.edu/u/j/jgross/.local64/coq/coq-polyproj/lib/coq/user-contrib/tmp1/tmp2/uu0test.vo contains libraryuu0test and not library tmp1.tmp2.uu0testif I coqc from tmp1/tmp2. If I fix it so that I don't get that error message, everything works fine, using the following script:#!/bin/bashcoqc --versioncoqc -whereCONTRIB="$(coqc -where)/user-contrib"echo "$CONTRIB"rm -rf user-contribmkdir user-contribcd user-contribmkdir -p tmp1/tmp2 tmp3rm -rf "$CONTRIB/tmp1"mkdir -p "$CONTRIB/tmp1/tmp2"echo 'Definition UU := Type.' > tmp1/tmp2/uuutest.vecho 'Require Export "uuutest".' > tmp1/tmp2/uu0test.vecho 'Require Export uu0test.' > tmp3/pathtest.vPS4='$ 'set -xcoqc -R tmp1 tmp1 tmp1/tmp2/uuutestcoqc -R tmp1 tmp1 tmp1/tmp2/uu0testcd tmp1/tmp2#coqc uuutest#coqc uu0testmv uuutest.vo uu0test.vo "$CONTRIB/tmp1/tmp2/"rm *cd ../../tmp3coqc pathtestOn Thu, Jan 2, 2014 at 11:34 AM, Vladimir Voevodsky <vladimir AT ias.edu> wrote:
If they start in user-contrib/tmp1/tmp2/ then there is no need to move them anywhere. Is your user-contrib/ in the lib/coq/ which Coq is using?This is the exact error message:moscow:tmp0 vladimir$ coqc pathstestFile "./pathstest.v", line 1, characters 0-25:Error: Cannot find library uuutest in loadpath(I am using mac and in my case the .vo files start somewhere far away from /opt/local/lib/coq/user-contrib/ which is in my case the "official" user-contrib/ for Coq)V.On Jan 2, 2014, at 10:52 AM, Jason Gross wrote:The *.vo files start in user-contrib/tmp1/tmp2, so I don't think they end up there. If I put them in user-contrib/tmp1, I get that "Error: Can't find file uu0test.vo on loadpath". I cannot imagine how you got "Cannot find library" rather than "Can't find file" unless you did not use quotes somewhere. If you want me to look further into the issue, please give me a version of the following script which reproduces the error on your computer, and let me know exactly what the output of the file is. (If you use windows or mac rather than linux, let me know, and I can give you a windows version or, probably, a mac version (though this version might work with mac as well as linux.)#!/bin/bashcoqc --versionrm -rf user-contribmkdir user-contribcd user-contribmkdir -p tmp1/tmp2 tmp3echo 'Definition UU := Type.' > tmp1/tmp2/uuutest.vecho 'Require Export "uuutest".' > tmp1/tmp2/uu0test.vecho 'Require Export uu0test.' > tmp3/pathtest.vPS4='$ 'set -xcd tmp1/tmp2coqc uuutestcoqc uu0testmv uuutest.vo uu0test.vo ../../tmp1/rm *cd ../../tmp3coqc pathtest-JasonOn Thu, Jan 2, 2014 at 9:42 AM, Vladimir Voevodsky <vladimir AT ias.edu> wrote:The files *.vo should go to user-contrib/tmp1/tmp2/ not to tmp3/V.On Jan 1, 2014, at 9:43 PM, Jason Gross <jasongross9 AT gmail.com> wrote:It works fine for me under those conditions, if I fix a few bugs in your code ([ : Type] to [:= Type], [Export "uuu"] to [Export "uuutest"], [Export "uu0test.v"] to [Export "uu0test"], adding periods:jgross@cagnode17:/tmp$ cat mk-uu.sh#!/bin/bashrm -rf tmp1 tmp3mkdir -p tmp1/tmp2 tmp3echo 'Definition UU := Type.' > tmp1/tmp2/uuutest.vecho 'Require Export "uuutest".' > tmp1/tmp2/uu0test.vecho 'Require Export "uu0test".' > tmp3/pathtest.vPS4='$ 'set -xcd tmp1/tmp2coqc uuutestcoqc uu0testmv uuutest.vo uu0test.vo ../../tmp3/rm *cd ../../tmp3coqc pathtestjgross@cagnode17:/tmp$ ./mk-uu.sh$ cd tmp1/tmp2$ coqc uuutest$ coqc uu0test$ mv uuutest.vo uu0test.vo ../../tmp3/$ rm uu0test.glob uu0test.v uuutest.glob uuutest.v$ cd ../../tmp3$ coqc pathtestjgross@cagnode17:/tmp$When you run this script, what output do you see? If you get the error with this exact script, what version of Coq are you using?On Wed, Jan 1, 2014 at 8:01 PM, Vladimir Voevodsky <vladimir AT ias.edu> wrote:Sorry, I have messed it up a bit. One should compile uuutest and uu0test from tmp2 not from tmp1. Also do not forget to remove the .vo files from tmp2 before attempting to compile pathtest.If this is done then the behavior is reproduced (an error unless the line "Require Import "uuutest"." is added to path test.v).Vladimir.On Jan 1, 2014, at 7:29 PM, Vladimir Voevodsky wrote:Do not use the user-contrib files which you have - they are not appropriate for the example.Simply create files:1. uuutest.v withDefinition UU:Type.2. uu0test.v withRequire Export "uuu".in tmp1/tmp2/3. pathtest withRequire Export "uu0test.v"in tmp3/Then docoqc tmp2/uuutestcoqc tmp2/uu0testfrom tmp1/Then copy tmp2/uuutest.vo and tmp2/uu0test.vo to user-contrib/tmp1/Then docoqc pathtestfrom 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.