[isabelle-dev] Isabelle2013-2 release

Makarius makarius at sketis.net
Thu Nov 21 13:11:57 CET 2013


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