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