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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev