coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Kirill Taran <kirill.t256 AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Dot-qualifying
- Date: Thu, 24 Jul 2014 14:05:31 +0400
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.
> 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
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 viaHave you compiled B first?
> 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.
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
- [Coq-Club] Dot-qualifying, Kirill Taran, 07/24/2014
- Re: [Coq-Club] Dot-qualifying, Cedric Auger, 07/24/2014
- Re: [Coq-Club] Dot-qualifying, Cedric Auger, 07/24/2014
- Re: [Coq-Club] Dot-qualifying, Pierre-Evariste Dagand, 07/24/2014
- Re: [Coq-Club] Dot-qualifying, Kirill Taran, 07/24/2014
- Re: [Coq-Club] Dot-qualifying, Kirill Taran, 07/24/2014
- Re: [Coq-Club] Dot-qualifying, Cedric Auger, 07/24/2014
- Re: [Coq-Club] Dot-qualifying, Kirill Taran, 07/24/2014
- Re: [Coq-Club] Dot-qualifying, Cédric, 07/25/2014
- Re: [Coq-Club] Dot-qualifying, Vladimir Voevodsky, 07/25/2014
- Re: [Coq-Club] Dot-qualifying, Cédric, 07/25/2014
- Re: [Coq-Club] Dot-qualifying, Kirill Taran, 07/24/2014
- Re: [Coq-Club] Dot-qualifying, Cedric Auger, 07/24/2014
- Re: [Coq-Club] Dot-qualifying, Kirill Taran, 07/24/2014
- Re: [Coq-Club] Dot-qualifying, Kirill Taran, 07/24/2014
Archive powered by MHonArc 2.6.18.