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

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

isabelle-dev mailing list

Reply via email to