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 editing.

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 icons.

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.


	Makarius


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.