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
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
