The Coq mailing list

[Kirill Taran <kirill.t256 AT gmail.com>]

Cedric,

Yes, that is true. But my question is about other:
I have done "coqc -I A -as A A/B.v" and "coqc C.v", where C.v contains "Require Import A.B."
And these commands suceeded, so latter command "coqc C.v" sees file A/B.v.

The question is: "How does "coqc C.v" see A/B.v without providing loadpath?".
Does coqc look into subdirectories for compiled files?

Sincerely,
Kirill Taran

On Thu, Jul 24, 2014 at 4:38 PM, Cedric Auger <sedrikov AT gmail.com> wrote:

2014-07-24 12:13 GMT+02:00 Kirill Taran <kirill.t256 AT gmail.com>:

> But it's probably wiser to use coq_makefile to have these things
generated for you.
Agree, I just wanted to get knowledge about the principle.

> Maybe it could help you to understand the compilation mechanism of Coq.
Yep, I hadn't recalled about this, I could generate Makefile and explore it for the proper commands.

By the way, I don't understand fully the principle:
When I type "coqc C.v", how does coqc determine that it must look into directory "A"?
If it just uses logic "A.B means A/B.v" then why do we need this stuff with "-I A -as A"?

I haven’t compiled projects for some time, but as far as I can remember, compiling a file needs "loadpaths", that is a set of directory considered as root for Coq.
Basically, that is what "AddLoadPath" (inside of files) or "-I" (inside of command line) is for.
"AddLoadPath" is useful when developing a short project and you do not want to write a Makefile, or change it each time you add/remove files.
Still it has portability issues (case sensitiveness and '/' vs '\' according to Windows vs Posix conventions), thus once you want to publish your project, you should use only the "-I" command line option.
Several paths can be set as the Coq root (useful to have both the standard library and your project files available).

If I remember well, in your case, instead of "-I A -as A" you could also have used "-I ." ("adds current directory to loadpath"). It would have been slightly different though: you would also have loaded all other directories than A.
And using "-I A" would have been different of "-I A -as A", as module B would have been considered at top level ("Require B." rather than "Require A.B.").
 

Sincerely,
Kirill Taran

On Thu, Jul 24, 2014 at 2:05 PM, Kirill Taran <kirill.t256 AT gmail.com> wrote:

Cedric and Pierre,

> In fact, that's were the magic happens: you must compile B.v
> (which is in the physical path "./A/") onto the logical path "A."

> coqc -I A -as A A/B.v

That is solution! Thanks.

I had compiled B when I was writing here, but I did it with plain "coqc A/B.v".
Now everything is clear, thanks.

Sincerely,
Kirill Taran

On Thu, Jul 24, 2014 at 12:28 PM, Pierre-Evariste Dagand <pedagand AT gmail.com> wrote:

> I tried to do simplest project with possibility to access modules via
> dot-notation:
> $ mkdir A
> $ touch A/B.v
> $ echo "Require Import A.B." >> C.v
>
> And I try "coqc -I A C.v", "coqc -I A -as A C.v"
> and "coqc -R A A C.v", but without success.

Have you compiled B first?

In fact, that's were the magic happens: you must compile B.v (which is
in the physical path "./A/") onto the logical path "A." (the jargon is
defined there [http://coq.inria.fr/distrib/current/refman/Reference-Manual016.html#sec568]).
To do so, you can either use :

coqc -I A -as A A/B.v
# Non-recursive import

or

coqc -R A A A/B.v
# Recursive import

Then, you simply compile C.v in the current physical and logical path:

coqc C.v


But it's probably wiser to use coq_makefile to have these things
generated for you.


Cheers,

--
Pierre

--
.../Sedrikov\...