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