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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
