On Monday 06 December 2010 15:38:07 Hendrik Tews wrote:
> I don't understand. Could you elaborate? Why is every file
> compiled twice?
Processing a coq file within emacs means feeding the file to coqtop step by
step. Compiling the file with coqc does pretty much the same thing with the
difference that if there's no error, a .vo file is produced.
Say you've got two files, A.v and B.v, and module A is required within module B
and now you need to edit file A.v somewhere in the middle. When you're finished
editing it in emacs and you process your changes with proofgeneral and you're
happy because everything went well, you have to re-process the whole file using
coqc to compile it to a .vo file.
That's why you don't bother processing the whole file, if you know that your
changes don't affect the rest of it.
This is the current situation but maybe, if proofgeneral could take advantage
of the coq state after having processed a whole buffer to create a .vo, then
this would be really interesting. But I have no idea about if/how this could
PhD Student - CEA-LIST Software Safety Lab. / INRIA ProVal Project
ProofGeneral-devel mailing list