[isabelle-dev] Isabelle2013-2 release

[Makarius]

On Thu, 21 Nov 2013, Peter Lammich wrote:

> From your description, this looks like a timeout-problem to me ... while 
> your machine is loaded by proving the theory, quickcheck times out. 
> After the edit, there is less load, and quickcheck is faster.

Yes, this is also my first guess.

Real-time limits always introduce erratic behaviour, as we knew already 
when these facilities were cultivated in Isabelle/ML some years ago (with 
the TimeLimit module).

In TTY / Proof General mode, the system is doing nothing until the user 
steps over the next command.  All CPU resources are idle and then rush 
through a single execution with various add-ons.  This makes it relatively 
deterministic.

In the PIDE document model, the system is doing many things all the time. 
Thus static assumptions about availability of CPU resources no longer 
hold.  The discussion about sledgehammer parameters based on numbers of 
CPU cores illustrates the problem further, e.g. see the isabelle-users 
thread "sledgehammer in RC4" 
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2013-November/msg00050.html


 	Makarius