[isabelle-dev] \nexists

[Lars Hupel]

> 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