Re: [PG-devel] speed up Coq Proof General by processing complete proofs
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 all prompts and link each of them to the corresponding command. If we hide the prompts then backtracking inside chunks will be impossible. Well, there is no backtracking to a position inside a proof once you finished the proof. So if a chunk is a whole proof, you loose nothing. Otherwise, I would say, if you switch on the speedup-option for processing in chunks, then you loose the ability to backtrack inside the chunks. If you want to go there, you have to backtrack the whole chunk and then start asserting again in smaller steps. Similarly to what you have to do now when you want to go into the middle of a proof after finishing it. Dealing with errors, as David said, will be a mess. Indeed. My plan would be the following: Before processing a chunk I remember the chunk start position somewhere. If there is an error inside the chunk I backtrack to the beginning of the chunk. I am pretty sure that this can work out without creating a mess. On the problem of speeding up pgcoq Hendrik please consider waiting for the next big change in Coq kernel: asynchronism. Or at least proof lazy evaluation. I have seen a prototype of that (by Enrico Tassi) and it surely will make pg and any other interface much faster from the user perspective I believe that these changes will speed up the compilation of whole files, i.e. coqc. But I doubt they will speed up my 2000 line files. If Proof General is too slow to feed coqtop such that the latter saturates 1 of my 4 cores, how could I gain from more parallelism? On the contrary, processing bigger chunks, especially whole proofs, would certainly increase the chance to profit from these improvements. These results are indeed surprising. As I don't see why sending commands separately would speed down Coq, I guess pg is slow at interpreting prompts (see below). Maybe I should have a look at my code on this. It might be the case that I see this big speedup, because my tactics are too low level. For the measurement I disabled the parser cache and inserted the following hack into coq-script-parse-cmdend-forward at the end, where it returns 'cmd: (progn (if (save-excursion (forward-line 0) (looking-at " *Proof")) (progn (re-search-forward "Qed\\." limit t) (end-of-line))) 'cmd ) Further I inserted (message "QUEUE EMPTY at %s" (float-time)) inside proof-shell-filter-manage-output in the if where proof-shell-exec-loop returns with true. I processed the buffer with M-x eval-expression (progn (message "START %s" (float-time)) (proof-process-buffer)) The above measurement hack works only if - you first delete all Qed's inside comments - make sure each Qed / Defined is the last command on its line - add ``(* Qed. *)'' after each Defined If you send me a file, which you are interested in, I can easily do the measurements. Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] speed up Coq Proof General by processing complete proofs
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 doesn't require special modifications to standard read-eval-print loops. The last sentence is the main secret of success of Proof General: it did not require much from the prover, so everyone could easily participate (well almost: the HOL family is still not there yet). 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. Concerning the PIDE model, see also my recent paper "READ-EVAL-PRINT in Parallel and Asynchronous Proof-Checking" http://www.informatik.uni-bremen.de/uitp12/papers/paper-02.pdf which tries to explain important technical aspects of PIDE in terms of the classic TTY model, and give hints how to get beyond it. And indeed, most of the time and effort is spent in organizing document processing. Proof checking happens eventually, too, but a single long-running automated proof method is counterbalanced by thousands of tiny commands that need to be parsed, results printed etc. Moreover, I've recently made a little experiment with Coq 8.4 beta as PIDE backend. See also https://bitbucket.org/makarius/coq-clone/src/4b806b6e1757/README.PIDE https://bitbucket.org/makarius/isabelle-coq/src at rev 07c7fc8ba7bd Both taken together gives you a proof of concept: Isabelle/PIDE/jEdit as front-end, Coq as backend. The latter merely does tokenization of the input as in CoqIDE. The backend can be refined further without substantial changes in the implemented infrastructure. (This exercise of mine required merely 5 days working with the Coq sources. More will be needed to make it do actual proof checking.) If there was still enough Emacs love in the world we could surely have an Emacs mode for that! In 2004-2007 you were the one to suggest giving up Emacs, and using Eclipse instead. In some sense you were right, not with Eclipse but the underlying JVM platform. It is not very pretty, but one of the very few platforms that is available on Windows-Mac-Linux, has statically typed programming languages on it (e.g. Scala), and fully supports multithreaded multicore programming. In contrast, Emacs is just a single-threaded LISP machine with some editing facilities. It was always a challange to make proper use of it for non-trivial things -- Proof General is the most complex elisp application I've ever seen. But this also poses many portability problems, because the assumptions about the underlying Emacs version are quite strong. Proof General on Cygwin is hardly working for many years. Mac OS is also not first class citizen. I am curious to see what happens with Isabelle Proof General after I've renounced responsibility of it last fall. Did the new maintainers show up already (Larry Paulson and Jasmin Blanchette)? Makarius ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] speed up Coq Proof General by processing complete proofs
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 ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] speed up Coq Proof General by processing complete proofs
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. -- Lionel ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
