Re: [isabelle] Isabelle2013-2-RC3 available for testing
On Sun, 1 Dec 2013, Makarius wrote:
* More robust termination of external processes managed by Isabelle/ML:
support cancellation of tasks within the range of milliseconds, as
required for PIDE document editing with automatically tried tools
Some more notes on this: there was a very old race condition where the
external process, when cancelled too early, was not killed at all. This
was not relevant in the past, because cancellation happened only due to
relative long timeouts (seconds) not the user editing (milliseconds).
(This is why I always call the TTY loop "boring", instead of the genuine
interaction that happens in the PIDE document processing game.)
As a consequence, there could be these typical "eprover" processes being
left over, after some minutes or hours of editing with auto sledgehammer
enabled. The new scheme is much more robust, but without any claim for
100% certainty (which is very difficult to achieve with arbitrary POSIX
The effect was particularly bad on Windows, where process startup takes
approx. 100ms instead of 1..10ms on Unix, but it did happen on Unix in
practice as well. I was finally convinced when I saw a stray "java"
process due to auto nitpick on Linux, so it was neither the notorious
Windows platform nor the very special eprover with its sophisticated
internal signal handling.
Further practical notes on automatically tried tools in Isabelle/jEdit:
* The Isabelle option "threads" should be the physical number of cores.
On Intel hardware with hyperthreading this is doubled by default and
thus reduces editor reactivity by too many parallel tasks.
i3 has 2 cores
i5 has 2 or 4 cores
i7 has 2 or 4 or 6 cores
* "Auto methods", which is similar to the command 'try0', tends to burn
a lot of cycles. Its internal parallelization and the global auto
tool time-out probably require some rethinking: this is still too
close to TTY mode, where the CPU is mostly idle, and sometimes rushes
through a few parallel tasks on all available cores. In PIDE, the
prover does more things all the time -- similar to an operating
This archive was generated by a fusion of
Pipermail (Mailman edition) and