The Coq mailing list

[dz dz <sophiee_shao AT hotmail.com>]

I have compiled (.v) files successfully, after using "coqc.opt XX" command. 

Thank you all!
Ying

> Message: 1
> Date: Thu, 19 Apr 2007 12:25:18 +0200
> From: Pierre Courtieu 
> <pierre.courtieu AT cnam.fr>
> To: Edsko de Vries 
> <devriese AT cs.tcd.ie>
> Cc: ?? ?? 
> <sophiee_shao AT hotmail.com>,
>  
> Coq-club AT pauillac.inria.fr
> Subject: Re: [Coq-Club] (no subject)
>
> Le Thu, 19 Apr 2007 10:34:55 +0100,
> Edsko de Vries 
> <devriese AT cs.tcd.ie>
>  a ?crit :
>
> > Did you compile XX? As far as I know, Require Import only opens
> > compiled libraries. To compile XX, open it in coqide, then select
> > Compile -> Compile Buffer. Then try the import again; it should work.
> >
> > Edsko
>
> You should also make sure that the compiled file (.vo) is in the path.
>
> You can do that at launch:
>
> coqide -I <path> -I <path>
>
> or inside coqide by the command
>
> Add LoadPath "path".
>
> By default the current path (the path where the current file is) is in
> the path.
>
> Cheers,
> Pierre Courtieu
>
>
> --__--__--
>
> Message: 2
> Date: Thu, 19 Apr 2007 09:13:22 -0700
> From: Adam Chlipala 
> <adamc AT cs.berkeley.edu>
> To: =?GB2312?B?ZHogZHo=?= 
> <sophiee_shao AT hotmail.com>
> CC: 
> Coq-club AT pauillac.inria.fr
> Subject: Re: [Coq-Club] (no subject)
>
> dz dz wrote:
> > when I input "Require Import XX" the coqide show that :User error:
> > cannot find XX library in loadpath. Here XX means some coq file i
> > wrote before, it not belongs to the coq libraries.
> > Is it because I use coq under windows system? I tried put the file I
> > want to import under different directories,the command didn't work.
>
> "Require" loads compiled (.vo) files. You could compile your XX.v file
> with the command line 'coqc XX' to produce XX.vo, and then the"Require"
> should work if the .vo file is in the current directory. Otherwise, use
> the "Load" command instead.
>
>
> --__--__--
>
> Message: 6
> From: =?gb2312?B?x7Mgx7M=?= 
> <sophiee_shao AT hotmail.com>
> To: 
> Coq-club AT pauillac.inria.fr
> Subject: Re: [Coq-Club] (no subject)
> Date: Fri, 20 Apr 2007 13:51:37 +0800
>
>
>
>
> >From: Adam Chlipala 
> <adamc AT cs.berkeley.edu>
> >To: dz dz 
> <sophiee_shao AT hotmail.com>
> >CC: 
> Coq-club AT pauillac.inria.fr
> >Subject: Re: [Coq-Club] (no subject)
> >Date: Thu, 19 Apr 2007 09:13:22 -0700
> >
> >dz dz wrote:
> > > when I input "Require Import XX" the coqide show that :User error:
> > > cannot find XX library in loadpath. Here XX means some coq file i
> > > wrote before, it not belongs to the coq libraries.
> > > Is it because I use coq under windows system? I tried put the file I
> > > want to import under different directories,the command didn't work.
> >
> >"Require" loads compiled (.vo) files. You could compile your XX.v file
> >with the command line 'coqc XX' to produce XX.vo, and then the"Require"
> >should work if the .vo file is in the current directory. Otherwise, use
> >the "Load" command instead.
>
> I have tried to compile many (.v) files, but all the files can't be
> transformed to (.vo) format.I manipulated step by step as follows: open XX
> file-> select "compile"-> select "compile buffer". Then  coqide indicated
> that : compilation output: 'coqc' ¿Ú ¿Ú ¿Ú ......(with many squares) .I
> don't know what the problem is.
> I always use "Load" instead of the "Require" command , is there any
> difference between these two command?
>
> Best Regards,
> Ying
>
> _________________________________________________________________
> Ãâ·ÑÏÂÔØ MSN Explorer:   http://explorer.msn.com/lccn
>
>
> --__--__--
>
> Message: 7
> Date: Fri, 20 Apr 2007 09:17:18 +0200
> From: Pierre Courtieu 
> <pierre.courtieu AT cnam.fr>
> To: =?gb2312?Q?=C7=B3_=C7=B3?= 
> <sophiee_shao AT hotmail.com>
> Cc: 
> Coq-club AT pauillac.inria.fr
> Subject: Re: [Coq-Club] (no subject)
>
> Le Fri, 20 Apr 2007 13:51:37 +0800,
> dz dz 
> <sophiee_shao AT hotmail.com>
>  a ¨¦crit :
>
> > I have tried to compile many (.v) files, but all the files can't be
> > transformed to (.vo) format.I manipulated step by step as follows:
> > open XX file-> select "compile"-> select "compile buffer". Then
> > coqide indicated that : compilation output: 'coqc' ¿Ú ¿Ú
> > ¿Ú ......(with many squares) .I don't know what the problem is.
>
> You should compile files by hand on the command line to see the error
> messages. Probably you have to change all your Load commands by "Require
> Export".
>
> coqc filename.v
>
> you should have the "bin" directory of coq installation in your path.
>
> > I always use "Load" instead of the "Require" command , is there any
> > difference between these two command?
>
> Yes, Load actually reads and interpret the whole file, which is very
> slow. Require (Export) loads the compiled file, which is much faster.
> Moreover when using compiled files you can have several definitions
> with the same name in different files without problem (use
> "filename.name" to distinguish).
>
> You definitely should compile your files. The best way is to do it on
> command line with a makefile. You can use the coq_makefile tool which
> is included with coq. It seems you are under windows so you should
> probably install gnumake (http://www.steve.org.uk/Software/make/),
> unless you are under cygwin. I never use coqc under windows. If you are
> under linux, coq_makefile is what you need.
>
> Best regards,
>
>
>
> > Best Regards,
> > Ying
>
>
>
> --__--__--
>
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>
> End of Coq-club Digest

_________________________________________________________________
ÓëÁª»úµÄÅóÓѽøÐн»Á÷£¬ÇëʹÓà MSN Messenger:  http://messenger.msn.com/cn