<div dir="ltr">Hi Makarius,<div><br></div><div>I think everyone involved with this issue is interested in coming back to a situation where we have a solution that works for everyone.</div><div>Can we try to find a proposal for a change of the current infrastructure that accommodates for yours and others' missing requirements?</div><div><br><div class="gmail_quote"><div dir="ltr">On Mon, Apr 24, 2017 at 6:12 PM Makarius <<a href="mailto:makarius@sketis.net">makarius@sketis.net</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">On 24/04/17 14:46, Makarius wrote:<br>
><br>
> Are there users of it outside the TUM group?<br>
><br>
> What is good about it? What is bad about it?<br>
<br>
(1) To follow the line of Mira vs. Jenkins:<br>
<br>
  * My main use of Mira was to figure out which Isabelle version<br>
corresponds to which AFP version, when something was broken in AFP.</blockquote><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<br>
  * I did not find this information in Jenkins, when I was still<br>
spending more time on it last year.</blockquote><div> </div><div>Is what Dmitriy<span style="font-size:13px;color:rgb(33,33,33);font-family:"helvetica neue",helvetica,arial,sans-serif;font-weight:bold;white-space:nowrap"> </span>pointed out (the status page) sufficient? </div><div><br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<br>
  * For actual quasi-interactive testing I always use "isabelle build"<br>
directly on a local or remote machine, with incrementally updated global<br>
build state (heaps and logs). Here it is important to get results within<br>
approx. 20-30 min -- presently we are at > 30 min.<br></blockquote><div><br></div><div>We can think of multiple solutions to bring down the testboard build times to 'quasi-interactive'.</div><div>This could also include incremental builds for the distribution if wanted.<br></div><div>Would you use the testboard if this was possible?</div><div><br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<br>
(2) To follow the line of Jenkins vs. isatest:<br>
<br>
When Jenkins was about to supersede isatest last year, I put forward<br>
missing requirements e.g. here:<br>
<a href="http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg06783.html" rel="noreferrer" target="_blank">http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg06783.html</a></blockquote><div><br></div><div>Let me restate these:</div><div><br></div>* 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.</div><div class="gmail_quote"><br></div><div class="gmail_quote">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 <span style="color:rgb(33,33,33);font-size:13px">to get rid of spurious failures in this setting (as Lars pointed out below)?</span></div><div class="gmail_quote"><br></div><div class="gmail_quote">* Decent performance measurements and charts: both multi-core run-time and heap space requirements.</div><div class="gmail_quote"><br></div><div class="gmail_quote"><div>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?</div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><br>
<br>
Today we have already the isatest sucessor "isabelle_cronjob" in<br>
Isabelle/Scala, and a proper discussion wrt. Jenkins needs to continue<br>
there. See also<br>
<a href="http://isabelle.in.tum.de/repos/isabelle/file/f8681c62959d/src/Pure/Admin/isabelle_cronjob.scala" rel="noreferrer" target="_blank">http://isabelle.in.tum.de/repos/isabelle/file/f8681c62959d/src/Pure/Admin/isabelle_cronjob.scala</a><br>
<br>
The latter is all about Isabelle administration infrastructure, i.e. the<br>
parts that are only seen when they don't work properly.<br>
<br></blockquote><div><br></div><div>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.</div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<br>
        Makarius<br>
<br>
_______________________________________________<br>
isabelle-dev mailing list<br>
<a href="mailto:isabelle-dev@in.tum.de" target="_blank">isabelle-dev@in.tum.de</a><br>
<a href="https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev" rel="noreferrer" target="_blank">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev</a></blockquote><div><br></div><div>Simon </div></div></div></div>