[isabelle-dev] HOL-Proofs slow

[Makarius]

On Mon, 22 Oct 2012, Florian Haftmann wrote:

>> HOL-Proofs has become very slow, see 
>> http://www4.in.tum.de/~wenzelm/test/stats/mac-poly64-M8/HOL-Proofs.png
>
> Btw. how do those graphs come into being?  The still official devel 
> snapshot page does not link there…

It is the normal output of Admin/isatest/isatest-stats.  I am eating these 
charts for breakfast since > 5 years.  For historical reasons, isatest 
does not publish these results when there is a failure, so it has to be 
done manually.  (This detail can probably now be changed, since "the" 
development snapshot that accompanies a successful isatest run has lost 
its purpose.)

These isatest statistics have proven to be essential to keep system 
performance in a reasonable range. So it is important to accumulated 
results continuously, even if they are not published on the spot.  My 
usual complaints about isatest not working for more than 2-3 days are 
motivated by the effect of becoming "blind" wrt. these performance 
measurements.

The Admin/isatest/settings are also carefully chosen (wrt. hardware, 
Poly/ML versions and options) such that certain aspects are measured, 
although this is far from exhaustive.  It is one of the traditional 
shortcomings of mira/testboard, that systematic measurement and statistics 
are missing.  Just this spring I ignored temporary "isatest blindness" 
before the Isabelle2012 release, with dire effects on the outcome (odd 
behaviour concerning signals masks and nohup).


 	Makarius