[isabelle-dev] Spike in isatest performance charts

[Makarius]

On Fri, 3 Sep 2010, Jasmin Christian Blanchette wrote:

> I added definitional CNF to Metis yesterday, which had a positive effect 
> on HOL and a neutral effect on the 1600 or so successful goals from the 
> Judgement Day suite. I'll revert this and reintroduce it if and when it 
> can be done without harming Metis_Examples (and other apps). (In fact, 
> Larry now suggested I avoid clausification altogether, which I will 
> investigate in the coming months.)

Does it mean it's from that changeset?

changeset:   39036:dff91b90d74c
user:        blanchet
date:        Thu Sep 02 11:29:02 2010 +0200
files:       src/HOL/HOL.thy src/HOL/Hilbert_Choice.thy src/HOL/SAT.thy 
src/HOL/Sledgehammer.thy src/HOL/Tools/Sledgehammer/clausifier.ML
description:
use definitional CNFs in Metis rather than plain CNF, following a suggestion by Joe Hurd;
this *really* speeds up things -- HOL now builds 12% faster on my machine


I know this temptation to "announce" things on the log only too well. 
Empirically, the reality is much harder.

When composing log messages it is important do this from the perspective 
of someone who needs to figure out problems many months/years later, and 
needs to understand what was truely happening at some point.  (Not so much 
what the author thought he was doing, or when the author went on vacation 
etc.)  Changelogs are neither NEWS nor personal Blog entries.


Anyway, are there any volunteers to bisect the persisting instablity of 
HOL-Decision_Procs/Approximation_Ex?  To me it looks like a long walk 
through recent history, and some extra opportunities to learn about 
software quantum mechanics.


 	Makarius