[isabelle-dev] Uses of Jenkins at TUM

[Lars Hupel]

>   * My main use of Mira was to figure out which Isabelle version
> corresponds to which AFP version, when something was broken in AFP.
> 
>   * I did not find this information in Jenkins, when I was still
> spending more time on it last year.

This information is all there. Build status is accessible via the
Jenkins API, of which you are undoubtedly aware. We also had both public
and private conversations where I pointed out to you where this is
available.

The user-facing side of this is
<https://devel.isa-afp.org/status.shtml>, which broke sometime around
Isabelle/7ca8810b1d48 though no change of my own, but so far I haven't
had time to investigate what caused it. (All entries are marked as
"skipped".)

>   * For actual quasi-interactive testing I always use "isabelle build"
> directly on a local or remote machine, with incrementally updated global
> build state (heaps and logs). Here it is important to get results within
> approx. 20-30 min -- presently we are at > 30 min.

This has also already been discussed. The vast majority of people I
asked is interested in quick feedback about AFP, which the testboard
provides.

> When Jenkins was about to supersede isatest last year, I put forward
> missing requirements e.g. here:
> http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg06783.html

This has also already been discussed. Testing with x86 caused too many
spurious failures, even after countless hours of tweaking parameters. I
refuse to take flak for reducing build noise.