[isabelle-dev] Isabelle2013-2 release

[Peter Lammich]

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
end*})

  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