[isabelle-dev] Spike in isatest performance charts
makarius at sketis.net
Fri Sep 3 15:06:02 CEST 2010
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?
date: Thu Sep 02 11:29:02 2010 +0200
files: src/HOL/HOL.thy src/HOL/Hilbert_Choice.thy src/HOL/SAT.thy
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.
More information about the isabelle-dev