Search code examples
coq

How to compile Coq files with Proof General + Emacs?

Now that I am moving on from Software Foundations where everything is served on a platter I am having trouble figuring out how to set up my own projects. There are some instructions out there, but since I am just starting out I find this too complex when trying to set up a hello world program. Also I have some other issues.

hello.v

The way I've managed to compile an empty hello.v is by putting the above in the _CoqProject file and then running...

coq_makefile -o Makefile.coq -f _CoqProject

This makes the makefiles.

make -f Makefile.coq

This compiles the project, but I can't get make hello to work with just this and Proof General happens to use this when compiling individual files.

make hello.vo
make: *** No rule to make target 'hello.vo'.  Stop.

The above is what I get when I try compiling from Proof General.

What should I do here? What would be the simplest possible way to set up a project with an empty file for use with Proof General + Emacs?

-Q . VFA

Also, why does SF vol 3 work despite not having much in its _CoqProject file? It only has the above.

Solution

  • 2022 Update

    There is a template to create new projects and to generate the associated boilerplate: https://github.com/coq-community/templates

    Original answer

    Here's what a conventional setup looks like (it's not actually standardized, you will find variations in the wild, especially for old projects, and future projects with dune now supporting Coq):

    _CoqProject
Makefile
theories/
  hello.v

    With the following _CoqProject:

    -Q theories/ MyProject
theories/hello.v
# list paths to .v files here

    In particular, qualifying the project (-Q path/ ProjectName) avoids ambiguities (if the same module name is used elsewhere) and makes it easier to import from other projects later.

    And the following Makefile:

    build: Makefile.coq
    $(MAKE) -f Makefile.coq

Makefile.coq: _CoqProject
    coq_makefile -f _CoqProject -o Makefile.coq

.PHONY: build

    The build target is marked .PHONY to indicate that it's not meant to create a file/directory. This avoids problems when other tools create a build directory for whatever reason.

    Command line

    To build the whole project from the command line, type make (which is equivalent to make build by default because build is the first command of the Makefile).
    To build only one .vo file, for example theories/hello.vo, type make -f Makefile.coq theories/hello.vo. It must be listed in the _CoqProject (so that coq_makefile then puts it into Makefile.coq.conf).

    Proof General

    In Proof General there is an option "Compile Before Require", which does as its name says. (Coq > Auto Compilation > Compile Before Require)

    The coq-Compile command you seem to have been using appears abandoned given its current lack of configurability. coq-Compile calls make hello.vo, but there is no hello.vo target in the Makefile, which is the one make looks at by default, unless the -f option is set. One way to make this PG command work with that setup is to include the generated Makefile.coq inside the Makefile:

    # Add this line to Makefile to enable PG's "coq-Compile"
-include Makefile.coq

    I'm personally hesitant to do that because I don't really understand what's in Makefile.coq.

    Also, why does SF vol 3 work despite not having much in its _CoqProject file? It only has the above.

    All SF volumes work that way now. For interactive editing with Proof General/CoqIDE, only the -Q option matters (actually, -R and a few others too), not the filenames. The filenames are used by coq_makefile, but you could also change the invocation of coq_makefile to get the filenames from elsewhere, for example as direct command line arguments:

    # If _CoqProject only contains the -Q option
coq_makefile -f _CoqProject theories/hello.v