[isabelle-dev] Isabelle2013-2 release

[Peter Lammich]

On Do, 2013-11-21 at 12:21 +0100, Makarius wrote:
> On Wed, 20 Nov 2013, Lawrence Paulson wrote:
> 
> > Are there options that would reveal instances of this problem?
> 
> It happens whenever you have something still running, but continue 
> editing.  The running tasks are errorneously interrupted and thus look 
> finished, although the state is failed.  (This bad state is not rendered 
> specifically, because it is not supposed to happen.)

On my machine, there is also a second way to run into this Problem:
  Just load a theory with a diverging command, and wait long enough
  (nondeterministically, between tens of seconds and several minutes). 
  The command appears to finish, and the theorem's status is failed.


In an earlier message on this thread, you have posted a patch. However,
I cannot apply this patch to the development repository, nor does the
revision "db3d3d99c69d", which your patch refers to, exist.

So how and against what should I apply this patch?

--
  Peter

> 
> This means that it is hardly possible to edit serious proof developments 
> reliably in Isabelle/jEdit.
> 
> 
> The problem is going back to Isabelle/78693e46a237 (03-Sep-2013), which is 
> just at the start of the consolidation of a whole summer's work.
> 
> In Isabelle/88c6e630c15f (24-Sep-2013) the change of command spans for the 
> sledgehammer panel has exposed the dormant problem in a way that it 
> becomes apparent very easily.  (Thus the sledgehammer change did not 
> introduce it, as I've first thought.)
> 
> 
> I am a little disturbed that such a serious problem was undetected (or 
> unreported) for such a long time.  It shows that the Isabelle development 
> and release process no longer works reliably -- although I've spent about 
> the same time doing new things in summer versus getting the release ready 
> in autumn.
> 
> Another conclusion is that the majority of serious proof development is 
> still done in Proof General.
> 
> 
>  	Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev