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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
