[isabelle-dev] Uses of Jenkins at TUM

[Simon Wimmer]

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 <makarius at 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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


Simon
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20170425/b53dd468/attachment-0002.html>