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
_______________________________________________
Isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
