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

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.)



Attachment: pg-multiple-file-patch-2011-01-11
Description: Binary data

ProofGeneral-devel mailing list

Reply via email to