Dear Hendrik,
Many thanks for the patch! I hope some users will test it but there
aren't many on this list, you might like to advertise your web page on
the Coq mailing list, perhaps?
I'll try to take a look myself soon.
I hope to release PG 4.1 shortly to coincide with the Isabelle release
and had hoped your patch would be ready by then, but maybe not.
- David
On 11/01/11 15:07, Hendrik Tews wrote:
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
_______________________________________________
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
_______________________________________________
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
--
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
