> 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 continuously. > 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: <https://ci.isabelle.systems/jenkins/job/isabelle-repo/changes> 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 > repository). Still satisfied. > * Help to figure out quickly why a broken AFP stopped working. When > did it work last time with Isabelle? Still satisfied. > * 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? Cheers Lars _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev