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
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
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
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.)
This archive was generated by a fusion of
Pipermail (Mailman edition) and