[isabelle-dev] Spike in isatest performance charts

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Fri Sep 3 13:45:06 CEST 2010

>> Today's isatest indicates a significant drop in performance:
>> http://isabelle.in.tum.de/devel/stats/at-poly/HOL-Metis_Examples.png
>> http://isabelle.in.tum.de/devel/stats/mac-poly-M4/HOL-Metis_Examples.png
>> http://isabelle.in.tum.de/devel/stats/mac-poly-M8/HOL-Metis_Examples.png
> 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.)

From my experience, when the performance of metis examples changes, this
might very well just due to one or two particular metis calls.  It might
be worth examining those.




PGP available:

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20100903/c30bc9ab/attachment.sig>

More information about the isabelle-dev mailing list