[isabelle-dev] Regain AFP sanity

Makarius makarius at sketis.net
Wed Jan 11 23:03:08 CET 2012


This is what I've produced in the meantime for AFP:

changeset:   2646:3dcc6b9eae2b
tag:         tip
user:        wenzelm
date:        Wed Jan 11 21:30:05 2012 +0100
summary:     method "cond_eval" reduces total runtime to a few minutes if 
FLYSPECK_SKIP_PROOFS=true;

Here is an example timing with my usual settings on macbroy2:
Finished HOL-Flyspeck-Tame (0:03:39 elapsed time, 0:06:50 cpu time, factor 1.87)

I've found this very convenient for quick feedback of AFP problems -- 
doing it the old-fashioned way on a fast machine by hand.


 	Makarius



More information about the isabelle-dev mailing list