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)?


ProofGeneral-devel mailing list

Reply via email to