[isabelle-dev] Spike in isatest performance charts

[Jasmin Christian Blanchette]

Am 03.09.2010 um 13:37 schrieb Makarius:

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

Thanks for spotting this and letting us know!

Jasmin