[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