Adding Multiple File Support for Coq Proof General

Multiple file support for Coq Proof General has now been released with Proof General 4.1. The new features as well as the current limitations are now documented in Section 10.2 Multiple File Support [for Coq] in the Proof General manual.

Download / Installation

Install Proof General version 4.1 and follow the hints about enabling automatic compilation in Section 10.2 Multiple File Support [for Coq] in the Proof General manual.


There is a new hook that is called just before items are put into proof-action-list. coq-mode adds a function to this hook that searches for require commands. If one is found dependency checking and recompilation is directly started. That is, recompilation takes place before all asserted items are really placed into the queue.

To compute the name of the file that possibly must be recompiled ProofGeneral uses coqdep. Therefore, with Coq version prior to 8.3pl2, Require Le does work but Require Arith.Le does not.

Internal mode uses coqdep and coqc in a straightforward recursive dependency traversal.

Discarded Implementation Options

Query coq instead of using coqdep
Does not work because there is no reliable way of translating a module name into a file name in coq. Locate Library fails if only the source file of the library is present. Locate File does not take the logical path into account, so its result does not make sense at all.
Traverse the load path in Proof General instead of using coqdep
Doable, but very complex. Just have a look at the coq code that deals with the load path!
Recompiling from inside the process filter that processes waiting items on proof-action-list
This makes error reporting much more difficult, because the errors are detected asynchronously inside the process filter. Further, when ProofGeneral is processing items from proof-action-list one cannot query the proof assistant, for instance for the current LoadPath.


Please send your comments and suggestions to ProofGeneral-devel mailing list or to

last modified on 4 Oct 2011 by Hendrik