[isabelle-dev] NEWS: sightly more parallel checking

[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 diagnostic commands (code_thms, export_code foo in SML), but those were not present anymore when I observed this 4-second-consolidation-loop.

The consolidation operates on the whole theory graph, even if relatively
little has actually happened. For a large session this might be expensive.

I have now changed this in Isabelle/2fd3a6d6ba2e, and tested it with
HOL-Library, HOL-Analysis, HOL-Probability, even with updates of the
State panel in between.

So far it looks good to me. Please keep me updated if there are
remaining problems.


	Makarius