[isabelle-dev] Build time for Isabelle/HOL (was: Aquamacs emacs)

[Makarius]

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 
performance statistics.

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

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/at-poly.html 
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 
required.

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:

   http://scala-webapps.epfl.ch/hudson/
   http://hudson-ci.org

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.


 	Makarius