On Thu, Aug 09, 2012 at 11:26:55AM +0200, Hendrik Tews wrote:

> I therefore tested the following idea: When Proof General
> processes larger chunks, it can send proof scripts as a whole
> instead of sending single tactics. The results were rather
> surprising:

> There are of course a number of problems to solve before Proof
> General is really able to process proofs, sections or modules as
> one chunk. But with the prospective speed improvement I would
> like to explore this idea further.

> I believe the first problem to solve is that of multiple prompts:
> When Proof General sends several statements together, coqtop
> answers with several prompts instead of one prompt. AFAICT there
> is no command to change or disable the prompt in coqtop.

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?

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

ProofGeneral-devel mailing list

Reply via email to