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.
Implementation
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.
Contact
Please send your comments and suggestions to ProofGeneral-devel mailing list or to
hendrik@askra.de
last modified on
4 Oct 2011
by Hendrik