On Tue, Mar 18, 2014 at 12:55 PM, Makarius <makar...@sketis.net> wrote: > Are you actually working together with Johannes Hölzl on these parts, or is > your later change 32b7eafc5a52 merely a coincidence?
We are not working directly together, but I suppose that the same email conversation with Larry Paulson has motivated both of us separately to clean up the Multivariate_Analysis theories. > Did you notice practically relevant performance issues with the > HOL-Multivariate-Analysis sessions? It is one of the (relatively few) > sessions where the fact name space change (for semantic completion) has > significant impact. I am still reading the tea leaves in the charts at > http://isabelle.in.tum.de/devel/. It is not yet clear to me, why this > session suffers more than others. I haven't noticed anything; but I suppose I have not been compiling the theories regularly enough to notice any performance patterns at all. Do you see the slowdown in batch mode, interactively, or both? - Brian _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev