Hi, below is a first patch against ProofGeneral version 4.0, that adds support for multiple files for coq. The patch is not complete yet, I would not expect an inclusion in the development version of ProofGeneral at this time. I post the patch to give you something to experiment with and to get some feedback.
The patch adds a hook to proof-extend-queue such that I can search for Require commands just before they are added to the queue. If I find a require I immediately check dependencies and recompile if necessary. Checking and recompilation is either done in a rather straightforward recursive function (coq-make-lib-up-to-date) or through an external command, configured with coq-recompile-command. For mapping module names to files I use an emacs hash table that models the LoadPath. It gets initialized in proof-shell-init-hook. The patch also adds an option proof-no-fully-processed-buffer, through which coq-mode does now require to fully retract even those buffers that have been completely asserted. There is lots to be done, see http://askra.de/software/multiple-coq/ for known problems. In particular I have not (yet) done any integration with the multiple file support that was there before. I abandoned the following two ideas: - Query coq to map module names to files There is apparently no reliable way to do this. - Do checking/recompilation from inside the process loop The main argument for this approach is that Add LoadPath commands have been processed before starting the dependency analysis. However, nobody is using Add LoadPath, and the argument is therefore a bit weak. On the contrary, error reporting is very complicated ... (I checked all coq user contributions, they only contain "Add LoadPath ".." twice for some examples in a subdirectory.) Bye, Hendrik
Description: Binary data
_______________________________________________ ProofGeneral-devel mailing list ProofGeneralfirstname.lastname@example.org http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel