[isabelle-dev] HOL-Decision_Procs FAILED

[Lawrence Paulson]

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.brian.c at gmail.com> wrote:

> 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
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev