[isabelle-dev] Spike in isatest performance charts

Jasmin Christian Blanchette jasmin.blanchette at gmail.com
Sat Sep 4 10:42:20 CEST 2010

> 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.

And public mailing lists are not the best place to criticize your colleagues' writing style.


More information about the isabelle-dev mailing list