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 ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
