[isabelle-dev] Non-slow AFP sessions

[Makarius]

Thanks to lots of performance tuning for Poly/ML 5.7.1, both
HOL-ODE-Numerics and HOL-ODE-Examples have become non-slow (see
AFP/13b569160947).

Here is the reference timing on rather old lxbroy7, which is also a
regular test machine for http://isabelle.in.tum.de/devel/build_status/AFP:

Finished HOL-ODE-Numerics (1:07:18 elapsed time, 1:07:17 cpu time,
factor 1.00)
Finished HOL-ODE-Examples (1:05:43 elapsed time, 1:05:42 cpu time,
factor 1.00)

Approx. 1h CPU time is de-facto the upper bound for non-slow sessions.
On more current multicore hardware these sessions are much faster,
especially when run in isolation on many cores. E.g. see the last
measurements as "slow":
http://isabelle.in.tum.de/devel/build_status/AFP_slow_64bit_6_threads/index.html#session_HOL-ODE-Examples


The idea general idea of non-slow AFP sessions: anything that can be run
routinely in interactive tests, e.g. after HOL library maintenance. It
should all finish in approx. 1h on high-end hardware (such as lxcisa0).

In the past 12 years, there has been a continuous challenge to keep up
with the natural growth of AFP applications. So far we have always
managed, and still do quite well.

I am also glad that the recent years of "flying blind" are over: we have
tangible performance data for all of AFP again, even a bit better than
in the past (individual ML statistics and theory timing).


	Makarius