[isabelle-dev] Uses of Jenkins at TUM

Makarius makarius at sketis.net
Mon Apr 24 18:12:08 CEST 2017

On 24/04/17 14:46, Makarius wrote:
> Are there users of it outside the TUM group?
> What is good about it? What is bad about it?

(1) To follow the line of Mira vs. Jenkins:

  * 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.

  * 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.

(2) To follow the line of Jenkins vs. isatest:

When Jenkins was about to supersede isatest last year, I put forward
missing requirements e.g. here:

Today we have already the isatest sucessor "isabelle_cronjob" in
Isabelle/Scala, and a proper discussion wrt. Jenkins needs to continue
there. See also

The latter is all about Isabelle administration infrastructure, i.e. the
parts that are only seen when they don't work properly.


More information about the isabelle-dev mailing list