Re: [isabelle] Incomplete goal may cause proof methods of later goals to loop.
On Wed, 23 Apr 2014, Yannick Duchêne (Hibou57) wrote:
I remember Coq has a different way to handle this: there are explicit
forward and backward (in proof state) commands. The processed part of a
proof is not editable and one have to go backward to edit it, then go
forward again and resume up to the last proof statement. This is
sometime tedious, while clean.
That's a way too much different compared to what Isabelle users are
accustomed to. Personally, it happens I think about the Coq way when I
feel Isabelle process too much of invalid text during editing, while in
other cases, I enjoy the reactivity of feedback from Isabelle while
Funny that you see the difference of Coq vs. Isabelle today like that, as
someone who did not know Isabelle about 3 years ago, when Proof General
was still the default.
In 1998, David Aspinall started an important pan-European prover interface
project called "Proof General". He asked several prover experts to help
him connect their particular system to that still emerging and
revolutionary front-end. I was the one to do the Isabelle/Isar
connection, when Isar itself was just about to emerge.
Note that "... while clean" above does not really apply, especially for
Coq. The real prover syntax is too complex for Proof General and its
modest elisp code to guess what the text means to the prover process.
The Coq toplevel also has some legacy operations from the pre-Proof
General era that make this harder than in Isabelle, and some Coq users are
actually still using the TTY loop (which normally does not happen for
Isabelle, because the Isar language makes this hard).
15 years ago there were also various internal discussions about the key
concepts how the prover front-end and back-end processes should
communicate, and certain fundamental limitations were already
well-understood, imposed by accidental side-conditions of existing
provers and the Emacs LISP machine.
Much of that is forgotten to outsiders now, and many Proof General users
think of it as something that has to be exactly like it is, because they
have never seen anything else. This lack of imagination and stagnation is
escpecially frustrating for me when I see the Proof General clone n + 1,
with excactly the same limitations, and just some change in colors and
The PIDE project came out of this more about 6 years ago, and it has
required a bit longer than expected to make it all ready for prime time.
Today it is hard to imagine anybody still using Isabelle Proof General,
and de-facto there has been nobody else maintaining it for about 3 years.
This archive was generated by a fusion of
Pipermail (Mailman edition) and