<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body bgcolor="#FFFFFF" text="#000000">
<p>Hello all,<br>
</p>
<br>
First, I would like to thank Lars for the time he is spending on
Jenkins.<br>
<br>
<br>
<div class="moz-cite-prefix">On 24.04.17 17:47, Blanchette, J.C.
wrote:<br>
</div>
<blockquote type="cite"
cite="mid:9B4DBCA6-AAA9-48C8-B000-051218B3B7DA@vu.nl">
<pre wrap="">
</pre>
<blockquote type="cite">
<pre wrap="">On 24 Apr 2017, at 17:12, Andreas Lochbihler <a class="moz-txt-link-rfc2396E" href="mailto:andreas.lochbihler@inf.ethz.ch"><andreas.lochbihler@inf.ethz.ch></a> wrote:
Sure. Whenever I have to push something to the Isabelle repository, I use the Jenkins testboard installation to see whether something broke. It works more reliably than the previous testboard infrastructure, which often ignored some commits.
</pre>
</blockquote>
<pre wrap="">
The same applies to me (VU Amsterdam), and I believe Mathias Fleury (MPII Saarbrücken) is also a heavy user of Testboard when he modifies Isabelle (e.g. the multiset library).
>From a pure basic user's perspective, I don't see much of a difference between Mira and Jenkins. To me it's just Testboard, and most of the time it works, and then I'm happy. Sometimes Mathias just sends me a link to a patch he's pushed to Testboard for me to review, before he pushes it to Isabelle. That's also very useful.</pre>
</blockquote>
Indeed. (Actually, patches can be seen <a moz-do-not-send="true"
href="https://isabelle.in.tum.de/repos/testboard">here</a> or <a
moz-do-not-send="true"
href="https://bitbucket.org/isa-afp/afp-testboard">here for
AFP-testboard</a>, but both are unrelated to Jenkins).<br>
<br>
<blockquote type="cite"
cite="mid:490db4df-2448-93d9-1fdd-d983c11331df@sketis.net">
<pre wrap="">What is good about it?</pre>
</blockquote>
(I don't remember enough of the previous system to compare it to
Jenkins.)<br>
<ul>
<li>automatic testing (I have forgotten to add files a couple of
times).</li>
</ul>
<ul>
<li>timings (<a moz-do-not-send="true"
href="https://ci.isabelle.systems/statistics/isabelle-nightly-benchmark/index.html">https://ci.isabelle.systems/statistics/isabelle-nightly-benchmark/index.html</a>).
It is useful to see how it evolves over time.</li>
</ul>
<p><br>
</p>
<blockquote type="cite"
cite="mid:490db4df-2448-93d9-1fdd-d983c11331df@sketis.net">
<pre wrap=""> What is bad about it?
</pre>
</blockquote>
I am trying very hard to not break Isabelle and the AFP. Therefore,
I hate receiving an email of Jenkins telling me that I have broken
something.<br>
<ul>
<li>Spurious timeouts (like <a moz-do-not-send="true"
href="https://ci.isabelle.systems/jenkins/job/isabelle-nightly-mac/">nightly-mac</a>
currently). At some point, there were timeouts that appeared
after one of my changes, but I could not reproduce them (they
were related to timeouts of quickcheck). Interestingly, I am now
in the opposite situation: At home, I currently have a lot of
timeouts related to "export_code" in Refine_Imperative_HOL that
do not appear in Jenkins. I will send another email to the
mailing list related to that.</li>
</ul>
<ul>
<li>Testing both Isabelle and AFP changes would be nice. This is
especially important for multisets that are not widely used in
Isabelle: Most bad simp rule break the AFP, not Isabelle.<br>
</li>
</ul>
<br>
<br>
However, both problems are hard to solve and I am happy with the
current situation. I even run a Jenkins instance at home.<br>
<br>
<br>
<br>
Mathias<br>
<blockquote type="cite"
cite="mid:9B4DBCA6-AAA9-48C8-B000-051218B3B7DA@vu.nl">
<pre wrap="">
Jasmin
_______________________________________________
isabelle-dev mailing list
<a class="moz-txt-link-abbreviated" href="mailto:isabelle-dev@in.tum.de">isabelle-dev@in.tum.de</a>
<a class="moz-txt-link-freetext" href="https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev</a>
</pre>
</blockquote>
<br>
</body>
</html>