[isabelle-dev] Jenkins maintenance

[Lars Hupel]

There are a lot of different issues in this thread, so let's unpack them
separately.

> Technical decisions need real reasons, not buzzwords.

What's the buzzword?

> It happens to very few people, only every 1-2 years. Such incidents are
> not a problem and need not be taken into account of technical engineering.

The build history paints a different picture.

In an ideal world everyone would run "isabelle build -D $AFP -a -o
document=pdf" before pushing, but clearly that is impractical.

The alternative, giving developers direct access to the build machines
to test out manually before pushing, is slightly less impractical
overall, but it is not the preferred way by developers and it creates
significant administrative overhead.

> It wastes CPU resources that are missing for important tests: coverage
> of thread parameters and other platform options is presently at 10-20%
> of what the last isatest setup was doing (which was already in a state
> of decline). We are flying mostly blind for a long time.

That is not entirely true. Currently we cover 2, 6, and 8 threads on
Linux and both 32 and 64 bit. All other tools (GHC, OCaml, ...) are
uniformly available on all build machines and participate in regular
testing.

Missing Mac tests are not the fault of the infrastructure itself, but a
result of a difficult hardware situation, imposed by Apple. Still, I'm
working on it, as I've already told you earlier this month. However,
it's not a deal-breaker: Many Mac users routinely use the development
version; system bootstrapping or integration problems will get detected
very early even without automated testing. (That doesn't change the fact
that automated testing on Mac is imminent, hopefully early October.)

Missing Windows tests are not a new problem and require some engineering
effort to automate due to more difficult administration and security
concerns.

Admittedly, the management of ML_OPTIONS as an environment variable is
not ideal currently, but I think we came to an agreement about this
earlier this month.

> We have also lost the correlation of Isabelle vs. AFP.
> 
> In the past, there was usually an accidental pairing of both repository
> snapshots, because tests were started at a fixed time after midnight
> when nobody was pushing.
> 
> By recording the two repository ids together with the nightly build
> status, it is usually easy to find a working state of particular AFP
> entries, based on a suitable Isabelle version.

This is not true at all. The correlation between Isabelle and AFP has
never been better.

Finding out the latest status is as easy as visiting
<https://devel.isa-afp.org/status.shtml>, which includes the Mercurial
IDs, the build time, the build cause and the link to the full build log.

Even more information is available, as usual, through the Jenkins API.
The entire history is recorded and formally available (admittedly not in
the repository).

The only caveat is that the "slow" sessions don't participate here; but
even so, they break extremely rarely and their pairing to the Isabelle
repository is also available through Jenkins.

Cheers
Lars