[isabelle-dev] Isabelle2013-2 release

Peter Lammich lammich at in.tum.de
Thu Nov 21 14:56:50 CET 2013

Finally, here is another way how isabelle-release/5adc68deb322 (i.e.
after your first patch)
appears to have proven a non-theorem.
Load the following and just wait a moment until the tactic interrupts
due to stack-overflow. The theorem's status gets failed, but this is not
displayed in isabelle/jEdit, nor is there an error on the tactic-block.

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!

  ML {*
    fun stack_overflow a = a + 1 + stack_overflow a

  lemma f:False by (tactic {* let val _ = stack_overflow 0 in all_tac

  ML_val {*
    Thm.peek_status @{thm f}

-- Peter

On Do, 2013-11-21 at 13:11 +0100, Makarius wrote:
> On Thu, 21 Nov 2013, Peter Lammich wrote:
> > 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.
> I would guess that it is just another way to get edits applied eventually. 
> There are many timers in Isabelle/jEdit and the underlying Isabelle/Scala 
> infrastructure, e.g. for garbage collection of unused document versions.
> This is a highly interactive computer-game.  The first time in the history 
> of "ITP" that interaction really happens.
> > 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.
> This mail thread is about the release: 
> https://bitbucket.org/isabelle_project/isabelle-release
>  	Makarius

More information about the isabelle-dev mailing list