[isabelle-dev] Isabelle2013-2 release

[Makarius]

On Thu, 21 Nov 2013, Peter Lammich wrote:

> I think that is a clear indication that the status failed can happen 
> (stack-overflow, out-of-memory, what-so-ever), and should be displayed 
> in isabelle/jEdit!

After diagnosing the problem, I did put a note on my TODO list to make the 
status reports more defensive, to allow system disintegration on the ML 
side.  E.g. the current order of status messages assumes that some later 
bits of ML code have a chance to run.

This is just the normal process of continuous convergence of the system 
towards an increasingly better state, which is ongoing for some decades 
already.  (An attempt to "fix" it now will inevitably break other things.)


>  ML {*
>    fun stack_overflow a = a + 1 + stack_overflow a
>  *}
>
>  lemma f:False by (tactic {* let val _ = stack_overflow 0 in all_tac
> end*})
>
>  ML_val {*
>    Thm.peek_status @{thm f}
>  *}

The question here is if it is of practical relevance or just a synthetic 
example.  You could also raise Exn.Interrupt here directly.

The principle that Proof General and Isabelle/jEdit as interactive 
front-ends are not required to be fully authentic still applies -- until 
there is just one uniform document model for batch and interactive mode, 
and no TTY nor Proof General anymore.

If a breakdown happens as easily as editing the text, it is a problem. 
If it is merely a conceptual demonstration of breakability, if is not.


 	Makarius