[isabelle-dev] Build time for Isabelle/HOL (was: Aquamacs emacs)
makarius at sketis.net
Mon May 17 20:30:49 CEST 2010
On Mon, 17 May 2010, Brian Huffman wrote:
> On Mon, May 17, 2010 at 7:43 AM, Makarius <makarius at sketis.net> 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.
This is a brief overview of the situation concerning Isabelle builds and
In the very old times, everybody always had an eye on local test build
times before committing (what would be pushing now), and Larry had an
extra script to cross-check rough build times, to guess at the general
When thas was no longer feasible (at the point when main HOL suddenly
became 4 times slower and stayed like that for several weeks), I've set up
a script to produce statistics from the isatest logs, see
http://isabelle.in.tum.de/devel/stats/mac-poly-M4.html etc. I check these
charts manually every day an investigate spikes by manual bisection as
Of course, this can be done better, and Alex and Florian have worked on
some Python + Mercurial setup to keep a more fine-grained record of
measurements in correspondence to points in the history. If something
like this is up an running, one should als produce more frequent isatest
runs, to get more datapoints. (I still have this archaic habit to
postpone certain pushes, because I know isatest figures will get diluted
by other concurrent changes on the same day).
Another possibility is to set up a more professional "continous build
server", such as the one that the smart guys from EPFL are using:
This looks still reasonably in size and complexity, i.e. there is some
chance it would not cause too many adminsitrative problems of its own.
Nonetheless such tools require some time to look into them, which I don't
have right now. For me the most pressing renovation of the build process
will be a Scala version of isabelle usedir/make/makeall that does away
with these odd IsaMakefiles that are never correct.
More information about the isabelle-dev