Re: [isabelle-dev] NEWS: sightly more parallel checking

2018-06-05 Thread Makarius
On 05/06/18 14:54, Fabian Immler wrote: > >> What kind of theory is this? Many commands? Long-running / >> non-terminating commands? > In this particular case, it was a relatively short theory (300 lines) with no > long-running or non-terminating commands. I inserted and removed some >

Re: [isabelle-dev] NEWS: sightly more parallel checking

2018-06-05 Thread Fabian Immler
> Am 05.06.2018 um 14:47 schrieb Makarius : > > On 05/06/18 14:45, Fabian Immler wrote: >> >> The only way to stop this apparently is to invalidate something in the beginning of the (currently open) theory. >>> >>> It should be possible to achieve this effect by removing the

Re: [isabelle-dev] NEWS: sightly more parallel checking

2018-06-05 Thread Makarius
On 05/06/18 14:45, Fabian Immler wrote: > > >>> The only way to stop this apparently is to invalidate something in the >>> beginning of the (currently open) theory. >> >> It should be possible to achieve this effect by removing the concluding >> 'end' command. > Just now I was in the middle of a

Re: [isabelle-dev] NEWS: sightly more parallel checking

2018-06-05 Thread Fabian Immler
> Am 05.06.2018 um 13:39 schrieb Makarius : > > On 04/06/18 20:17, Fabian Immler wrote: >> >> This "something in the background" appears to happen on a regular basis: >> every 2-3 seconds, the poly process consumes 200%CPU for about a second. >> poly should be idle (or used to be in such a

Re: [isabelle-dev] NEWS: sightly more parallel checking

2018-06-05 Thread Makarius
On 04/06/18 20:17, Fabian Immler wrote: > > This "something in the background" appears to happen on a regular basis: > every 2-3 seconds, the poly process consumes 200%CPU for about a second. > poly should be idle (or used to be in such a situation) because (as far > as I can tell) nothing else

[isabelle-dev] NEWS: sightly more parallel checking

2018-06-03 Thread Makarius
*** Isabelle/jEdit Prover IDE *** * Slightly more parallel checking, notably for high priority print functions (e.g. State output). This refers to Isabelle/b00b40dc41af -- with various fine points in the organization of PIDE execution forks, not just the preceeding cd387c55e085. As we are