[isabelle-dev] Isabelle build status with timing information

[Lawrence Paulson]

Thanks for those graphs, which are really interesting. Note in particular the sharp drops in elapsed time or heap for Analysis, Probability, Algebra and several others. What gets the credit for this?

Larry

> On 10 May 2017, at 10:55, Makarius <makarius at sketis.net> wrote:
> 
> 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
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20170510/22c79498/attachment-0002.html>