[isabelle-dev] Uses of Jenkins at TUM
mathias.fleury at ens-rennes.fr
Tue Apr 25 09:41:46 CEST 2017
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
> 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).
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.
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the isabelle-dev