[isabelle-dev] Uses of Jenkins at TUM

[Mathias Fleury]

Hello all,


First, I would like to thank Lars for the time he is spending on Jenkins.


On 24.04.17 17:47, Blanchette, J.C. wrote:
>> On 24 Apr 2017, at 17:12, Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch> 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.
> 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.
Indeed. (Actually, patches can be seen here
<https://isabelle.in.tum.de/repos/testboard> or here for AFP-testboard
<https://bitbucket.org/isa-afp/afp-testboard>, but both are unrelated to
Jenkins).
 
> What is good about it?
(I don't remember enough of the previous system to compare it to Jenkins.)

  * automatic testing (I have forgotten to add files a couple of times).

  * timings
    (https://ci.isabelle.systems/statistics/isabelle-nightly-benchmark/index.html).
    It is useful to see how it evolves over time.


>  What is bad about it?
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.

  * Spurious timeouts (like nightly-mac
    <https://ci.isabelle.systems/jenkins/job/isabelle-nightly-mac/>
    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.

  * 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.



However, both problems are hard to solve and I am happy with the current
situation. I even run a Jenkins instance at home.



Mathias
> Jasmin
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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