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 
be done. 
Paolo Herms
PhD Student - CEA-LIST Software Safety Lab. / INRIA ProVal Project
Paris, France
ProofGeneral-devel mailing list

Reply via email to