[isabelle-dev] HOL-Decision_Procs FAILED
huffman.brian.c at gmail.com
Tue Mar 18 21:58:49 CET 2014
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?
More information about the isabelle-dev