[isabelle-dev] Spike in isatest performance charts

[Florian Haftmann]

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

	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

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