[isabelle-dev] Isabelle build status with timing information

[Makarius]

After a delay of some weeks (actually several months since October 2016)
there is now an updated version of the classic Isabelle build status
with timing information, see
http://isabelle.in.tum.de/devel/build_status and its source
http://isabelle.in.tum.de/repos/isabelle/annotate/96b4799a2e04/src/Pure/Admin/isabelle_devel.scala#l82


This demonstrates that it is still possible to produce performance
charts in the quality that we've known from the past. Two main factors
are relevant for this:

  (1) The physical measurements need to be done without disturbance by
other processes, especially no other test processes running in parallel
on the same CPU/memory node. (The numactl tool can be a great help.)

  (2) Data plotting requires care about the gnuplot installation. For
reasons that I don't understand, various Linux distributions (e.g
Gentoo) can show quite bad interpolation in gnuplot, and make the data
look worse than it really is. For the above, I have just compiled
gnuplot-5.0.6 from the original source and suddenly it worked smoothly.


The data for the charts is collected as plain log files for archival
purposes in /home/isatest/cronjob/log/ at TUM. This directory is
uploaded every day to a PostgreSQL database server in the background
(only accessible by "isatest"). It can then be used with tools like
"isabelle build_status" to make the charts.

In addition, there is a small database snapshot in SQLite format:
http://isabelle.in.tum.de/devel/build_log.db -- e.g. for exploration
with sqlitebrowser (which also supports minimal plotting). Here is an
example query for its "Execute SQL" window:

SELECT pull_date, heap_size FROM isabelle_build_log
WHERE session_name = 'HOL-Analysis' AND  build_host = 'lxbroy9' AND
threads = 1
ORDER BY pull_date

Comparing this with threads = 2 shows that heap images produced by a
multi-threaded build process are slightly bigger, which I did not know
before. So this is one of the usual starting points for performance and
resource usage tuning, based on such relevant performance measurements.


There is more in the data that is not plotted yet, e.g. the precise
relation of tests run with threads=1,2,4,6. Or online heap usage, thread
activity, future tasks, etc. for an individual process (ml_statistics).

At last we are no longer "flying blind" ...


	Makarius