[isabelle-dev] Isabelle2013-2 release
makarius at sketis.net
Thu Nov 21 12:31:52 CET 2013
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
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"
More information about the isabelle-dev