[isabelle-dev] HOL-Decision_Procs FAILED

[Brian Huffman]

On Tue, Mar 18, 2014 at 12:55 PM, Makarius <makarius at 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