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 file1.v ... filen.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 file1 ... filen, 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
Or see the man page of do_Makefile for more details.