Hi Makarius, I think everyone involved with this issue is interested in coming back to a situation where we have a solution that works for everyone. Can we try to find a proposal for a change of the current infrastructure that accommodates for yours and others' missing requirements?
On Mon, Apr 24, 2017 at 6:12 PM Makarius <makar...@sketis.net> wrote: > 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. Is what Dmitriy pointed out (the status page) sufficient? > * 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. > We can think of multiple solutions to bring down the testboard build times to 'quasi-interactive'. This could also include incremental builds for the distribution if wanted. Would you use the testboard if this was possible? > (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 Let me restate these: * Realistic tests with typical settings. This means that x86 (and not x86_64) is used by default. We've recently seen mysterious resource problems occasionally, and the automatic testing infrastructure should be able to point quickly to relevant changesets. We now have a periodic build job for x86, too. Why would you still opt for x86 as a default, considering it is very hard to get rid of spurious failures in this setting (as Lars pointed out below)? * Decent performance measurements and charts: both multi-core run-time and heap space requirements. Your point of criticism seems to be that the currently available charts are not as reliable as what was available many years ago. However, this seems to already have been a problem in the pre-Jenkins times. Can you suggest a scheme to get more reliable measurements? > > > 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. > > What I take away from this thread so far is that most users generally seem to be happy with the Jenkins infrastructure. Thus, we are happy to continue the discussion, but I do not see why we would need a completely different testing infrastructure. > > Makarius > > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev Simon
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
