I may partly be to blame by introducing some metis calls. But there are some terrible proofs here (e.g. just “rule”, WTF?).
Larry On 18 Mar 2014, at 20:58, Brian Huffman <huffman.bria...@gmail.com> wrote: > 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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev