[isabelle-dev] Isabelle2013-2 release

[Peter Lammich]

Addition: The stack-overflow problem already occurs in Isabelle2013,
however, the theorem's status is unfinished here, but isabelle/jEdit
also gives no indication of this.

--
  Peter

On Do, 2013-11-21 at 14:56 +0100, Peter Lammich wrote:
> 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
> 
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev