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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
