The main problem with your solution is that for the moment pg coq needs to
see the informations that were present in the prompt before a command was
issued to know how to back just before this command. Therefore if we want
to be able to backtrack inside the chunks we need to read al
On Thu, 9 Aug 2012, David Aspinall wrote:
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 d
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 pro
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 pr
Hi,
I was recently a bit annoyed by the time Proof General needs to
process my Coq files. A simple measurement showed that Proof
General has only one third or less of the speed of coqc.
I therefore tested the following idea: When Proof General
processes larger chunks, it can send proof scripts a
