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
   (e.g. Sledgehammer).

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 processes).

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 MHonArc.