[isabelle-dev] Isabelle2013-2 release

[Makarius]

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

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