[isabelle-dev] Uses of Jenkins at TUM

[Makarius]

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:
http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg06783.html

Today we have already the isatest sucessor "isabelle_cronjob" in
Isabelle/Scala, and a proper discussion wrt. Jenkins needs to continue
there. See also
http://isabelle.in.tum.de/repos/isabelle/file/f8681c62959d/src/Pure/Admin/isabelle_cronjob.scala

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


	Makarius