On Monday 06 December 2010 14:14:27 David Aspinall wrote:
> Pierre and I had investigated a few ideas,
> you can still see some code remains in coq.el from some old attempts
> that partly worked (auto-compile-vos), but it seemed that Coq users were
> never hugely interested in the feature.
It would be more interesting, if the compilation reused the coqtop state
obtained while processing the buffer. Currently every file is actually compiled
twice. So nobody would reasonably process the whole buffer after having edited
it somewhere in the middle just to trigger the automatic compilation.
Also, a completely processed buffer doesn't seem to be retracted when starting
to process another buffer. This is not what you want in Coq where the
environment remains polluted by the definitions made in the other module.
But the mechanism Hendrik proposes sounds very useful, so good luck!
PhD Student - CEA-LIST Software Safety Lab. / INRIA ProVal Project
ProofGeneral-devel mailing list