On Mon, May 17, 2010 at 7:43 AM, Makarius <[email protected]> wrote: > > Right now I am bisecting our repository as David suggested, which is an > interesting experience because last year's Isabelle/HOL builds really fast > (factor 2 compared to today).
A factor of 2 slowdown is quite significant, and also rather worrying. Part of the difference can be attributed to sheer size (my HOL image today is 123 MB, compared with 108 MB for 2009-1 and 89 MB for 2009) but there is still a significant slowdown yet to be accounted for. Are there any measurements we can do (e.g. profiling the entire build of Isabelle/HOL) that could help determine the cause of the slowdown? For libraries that haven't changed much in the last year, are their build times slower by a similar factor? I don't think users would be very pleased if the new version of Isabelle takes twice as long to process their old theories. Perhaps only theory files that use certain features (like defining type classes, maybe) are slowed down; how could we test this? - Brian _______________________________________________ Isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
