On 09/08/12 11:11, Lionel Elie Mamane wrote:

That's why (back when it was available), I preferred to use the
"coq-interface" protocol rather than the "coqtop -emacs" protocol,
which has chunking multiple commands cleanly. I haven't looked at it
recently, but it seems to be the PCoq interface protocol was moved to
the contribs, and can still be taken from there?

Yves Bertot asked me years ago why Proof General never used this mechanism, and at the time I wasn't convinced it was much of a saving over sending commands individually. The simpler mechanism was a least common denominator for different systems and doesn't require special modifications to standard read-eval-print loops.

These days it seems more likely that the communication would often dominate the processing time for a single command so batching on the prover side would clearly be a better mechanism. In fact, so is having the prover (or some intermediate component) manage the *whole* document, which is the PIDE model. If there was still enough Emacs love in the world we could surely have an Emacs mode for that!

But porting PG to it might be more hassle than useful, and possibly
the "Set/Unset Prompt" route would be more expedient.

Yes, probably... The thing to watch out for is the error behaviour, though. If one command in a batch fails, PG needs to know which command is responsible (or else that the prover considers the whole transaction failed).

 - D.

ProofGeneral-devel mailing list

The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

Reply via email to