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

Reply via email to