Paolo Herms <> writes:

   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 [...]

Thanks for the clarification. I would say the
processing-twice-problem is somewhat orthogonal to detecting
out-of-date vo files. The latter gives correctness and is also
important when you update files outside of emacs. The former is
an optimization problem, which I would approach later.

>From my experience with PVS I would hope that one can get
reasonable performance by skipping proofs when reprocessing files
during development. 


ProofGeneral-devel mailing list

Reply via email to