[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