12.3 Creating a Makefile for Coq modules

12.3 Creating a `Makefile` for Coq modules

When a proof development becomes large and is split into several files, it becomes crucial to use a tool like make to compile Coq modules.

The writing of a generic and complete Makefile may seem tedious and that's why Coq provides a tool to automate its creation, do_Makefile. Given the files to compile, the command do_Makefile prints a Makefile on the standard output. So one has just to run the command:

% do_Makefile file₁.v ... file_n.v > Makefile

The resulted Makefile has a target depend which computes the dependencies and puts them in a separate file .depend, which is included by the Makefile. Therefore, you should create such a file before the first invocation of make. You can for instance use the command

% touch .depend

Then, to initialize or update the modules dependencies, type in:

% make depend

There is a target all to compile all the files file₁ ... file_n, and a generic target to produce a .vo file from the corresponding .v file (so you can do make file.vo to compile the file file.v).

do_Makefile can also handle the case of ML files and subdirectories. For more options type

% do_Makefile --help

Warning: To compile a project containing Objective Caml files you must keep the sources of Coq somewhere and have an environment variable named COQTOP that points to that directory.