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
