The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

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/bash

rm -rf tmp1 tmp3

mkdir -p tmp1/tmp2 tmp3

echo 'Definition UU := Type.' > tmp1/tmp2/uuutest.v

echo 'Require Export "uuutest".' > tmp1/tmp2/uu0test.v

echo 'Require Export "uu0test".' > tmp3/pathtest.v

PS4='$ '

set -x

cd tmp1/tmp2

coqc uuutest

coqc uu0test

mv uuutest.vo uu0test.vo ../../tmp3/

rm *

cd ../../tmp3

coqc pathtest

jgross@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 pathtest

jgross@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 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.v

user-contrib/Foundations/Generalities/uu0.v

user-contrib/Foundations/Generalities/uuu.v

jgross@cagnode17:/tmp$ cat user-contrib/Foundations/Generalities/uuu.v

jgross@cagnode17:/tmp$ cat user-contrib/Foundations/Generalities/uu0.v

Require Export "uuu".

jgross@cagnode17:/tmp$ cat user-contrib/pathnotations.v

Require Export "uu0".

jgross@cagnode17:/tmp$ coqc user-contrib/Foundations/Generalities/uuu.v

jgross@cagnode17:/tmp$ coqc user-contrib/Foundations/Generalities/uu0.v

File "./user-contrib/Foundations/Generalities/uu0.v", line 1, characters 0-21:

Error: Can't find file uuu.vo on loadpath

-Jason

On 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