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 as a whole
instead of sending single tactics. The results were rather

sample                                    1 proof      file         file 
                                        (200 lines) (2050 lines) (3400 lines)

coqc                                         -       7.1 sec       6.5 sec
PG standard                               4.2 sec   21   sec      29   sec 
optimized PG processing whole proofs      0.05sec    5.4 sec       5.4 sec

The comparison with coqc is a bit unfair here, because in Proof
General I measured proof-process-buffer after asserting a first
comment in the file, thus, in the Proof General measurements,
starting coqtop was not included.

The optimized measurement is not completely accurate, because
Proof General got confused by seeing too much coq prompts and
therefore sent the material earlier than it should.

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. 

Pierre, do you think there are changes to get a Set/Unset Prompt
command included, which enables/disables prompt printing?


ProofGeneral-devel mailing list

Reply via email to