hupel at in.tum.de
Sat Jul 16 16:37:22 CEST 2016
> I am open to hear arguments why latex documents need to be continuously
> available. So far there were none.
That statement is unrelated to what you wrote afterwards, but let me
give you an argument anyway: The generated PDFs are, as you probably
agree, formal documents. In that sense, they need to be checked
> Instead we have in Isabelle/76492eaf3dc1 + AFP/89fba56726d8 a typical
> situation where formal checking no longer works, due to changes in main
> Isabelle that are not immediately clear.
But the situation is completely clear. Jenkins gives you an overview of
what exactly broke, by means of the "changes" page:
It even provides handy links to the changesets.
> In the last 10 years, continuous testing of Isabelle + AFP had the
> following main purposes:
> * Make sure that formal checking of Isabelle always works 100% (main
> * Help to figure out quickly why a broken AFP stopped working. When
> did it work last time with Isabelle?
> * Provide continuous performance measurements to keep everything going
> in the longer run: i.e. to avoid the "invisible concrete wall" that is
> always ahead of us, and moved occasionally further ahead.
The numbers are there, but we need some good way to evaluate them. I
have pointed that out multiple times.
Let me be very clear: I have invested a lot of time in a robust,
reliable, reproducible testing infrastructure. Almost everything now
uses standardized tools instead of ad-hoc Bash or Perl scripts and
consumes or produces structured data. But I cannot single-handedly
implement all the features. To give useful performance metrics, here are
some questions off the top of my head:
- Measure the whole build time or just sessions?
- Which sessions? What should be the minimum threshold for session
runtime to be considered useful?
- Elapsed time or CPU time?
- What about sessions that grow in size over time?
More information about the isabelle-dev