Re: [isabelle] jEdit apparantly proves False



On Wed, 20 Nov 2013, Makarius wrote:

I confirm that this is a serious problem.  Thanks for reporting this.

I need further digging in the sources and history to work to the bottom of it. I am also getting mentally ready for another release very soon.

The situation is indeed so bad that I am about to produce a new stable release of Isabelle2013-2 soon: the first (and probably only) release candidate is scheduled for Sun 24-Nov-2013 and the final release for Sun 01-Dec-2013.

So if there is anything else to report, there are a few days left to do it in a relaxed manner. Changing a formal release candidate next week requires more weight and gravity. The current state of affairs can be seen here https://bitbucket.org/isabelle_project/isabelle-release/commits


For completeness, here is a wrapup of the incident.

Formally, the interactive front-ends (Proof General, Isabelle/jEdit, or whatever), are not required to be fully authentic. Only batch builds really count at the end of the day. But a system that breaks down too easily is not a stable release. (This concept is taken seriously for Isabelle, against the tides of the time.)

Here the problem is that editing a running task with internal parallel forks can cause accidental interrupts, which are not reported as error to the front-end, because they should not happen under normal circumstances. So the proof status appeared OK on the surface, but the internal thm was in a "failed state" -- as correctly recorded by the LCF-kernel.

The source of the problem is twofold: (1) a genuine mistake in the implementation of the Execution.fork mechanism of PIDE, which caused the accidental interrupt of a running task (Sep-2013). (2) failure to report the interrupt as error on purpose (!) "to avoid confusion in log etc." as the changelog entry says (Oct-2012). The "log etc." refers to batch builds, TTY mode, and Proof General, which is easily confused by error messages coming in the wrong moment.


This illustrates again the problems of having too many old and new things in an increasingly complex system. I am trying for years to unify the batch build with the PIDE interaction model, which is difficult in its own right. The legacy interaction modes of TTY or Proof General are adding to the complication.

Last spring, I actually dismantled the old PGIP experiment, which greatly simplified the classic Proof General mode and recovered some long lost functionality. Likewise, a much greater relieve will happen when Proof General itself comes out of use and can be dismantled.

I've no idea how long it will take to sort it all out. The number of people who are still using Proof General is unclear to me. When traveling to ITP 2013 this summer, my guess was 40% Isabelle/jEdit vs. 60% Proof General among power users, but it turned out the opposite when traveling back home.

Maybe we should make a "coming out" session at ITP 2014: "My name is P. W. User, ... and I am still using Proof General" :-)

(Further elaboration Proof General issues deserve a separate mail thread.)


	Makarius




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