The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Hello,

The require command indeeds needs the corresponding .vo file. coqc
allows to generate a .vo file from a .v file. You should use it as any
compiler:

coqc <the options you need> file.v

and it will produce a file.vo. For the options see the coq
documentation. You probably do not need any option if your development
is not split into several directories.

As with any compiler you may be interested in automating the
compilation process, this is where make and makefiles are often used.
However I am afraid this mailing list is not dedicated to learning how
to use make. See makefile documentation on the web.

Notice there is a tool called coq_makefile to generate automatically a
makefile for a bunch of coq files. For more information see the coq
website (which seems down currently :().

Best regards;
Pierre Courtieu



2012/11/9 Wilayat Khan 
<wilayatk AT gmail.com>:
> Hello
>
> I have a Coq project with a number of files (say x1.v, x2.v, ... xn.v)
> including a Makefile stored in folder
> "C:\Users\WK\Desktop\Personal\coq-project" and have installed Coq 8.3 at
> "C:\Coq" on my Windows 7 machine.
>
> The Coq programs (files) are dependent on each other. How can I execute a
> single program (say x1.v) in Coq? I want to open a file in Coqide and
> compile line by line to understand it, but it gives errors as there are many
> imported files in each, with no one in (.vo) format. I think there is some
> use of commands coqc, coqtop, make or any combination of these but I dont
> know the exact format of commands, paths, arguments, and order. Please let
> me give complete commands with full paths keep in mind the above paths.
>
> Thanks,
>
> Wilayat