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

_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to