Re: [isabelle-dev] Uses of Jenkins at TUM

2017-05-15 Thread Makarius
On 25/04/17 09:41, Mathias Fleury wrote: > >> What is good about it? > (I don't remember enough of the previous system to compare it to Jenkins.) Lets go back to some points on this thread, now that I have finished more implementation work. > * automatic testing (I have forgotten to add

Re: [isabelle-dev] Uses of Jenkins at TUM

2017-04-28 Thread Makarius
On 24/04/17 14:46, Makarius wrote: > This is another attempt to open a discussion about Jenkins at TUM. Thanks to everyone who participated on this thread. I have learned a few new things, which I will pick up again soon. Makarius ___

Re: [isabelle-dev] Uses of Jenkins at TUM

2017-04-25 Thread Simon Wimmer
Hi Makarius, I think everyone involved with this issue is interested in coming back to a situation where we have a solution that works for everyone. Can we try to find a proposal for a change of the current infrastructure that accommodates for yours and others' missing requirements? On Mon, Apr

Re: [isabelle-dev] Uses of Jenkins at TUM

2017-04-25 Thread Lars Hupel
> * My main use of Mira was to figure out which Isabelle version > corresponds to which AFP version, when something was broken in AFP. > > * I did not find this information in Jenkins, when I was still > spending more time on it last year. This information is all there. Build status is

Re: [isabelle-dev] Uses of Jenkins at TUM

2017-04-25 Thread Dmitriy Traytel
Hi Makarius, > On 24 Apr 2017, at 18:12, Makarius wrote: > > On 24/04/17 14:46, Makarius wrote: >> >> Are there users of it outside the TUM group? My usage is the same as in Jasmin’s and Andreas’ case. >> >> What is good about it? What is bad about it? > > (1) To

Re: [isabelle-dev] Uses of Jenkins at TUM

2017-04-25 Thread 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 >> wrote: >> >> Sure. Whenever I have to push something to the Isabelle repository,

Re: [isabelle-dev] Uses of Jenkins at TUM

2017-04-24 Thread Makarius
On 24/04/17 18:10, Lars Hupel wrote: >> In parallel (before and after Mira) we've had the older isatest. I don't >> know if Mira ever had the ambition to replace isatest, but Jenkins tried >> to do all that and failed. This was the start of my great worries about >> the Isabelle administration and

Re: [isabelle-dev] Uses of Jenkins at TUM

2017-04-24 Thread Lars Hupel
> In parallel (before and after Mira) we've had the older isatest. I don't > know if Mira ever had the ambition to replace isatest, but Jenkins tried > to do all that and failed. This was the start of my great worries about > the Isabelle administration and release infrastructure ... So, you're

Re: [isabelle-dev] Uses of Jenkins at TUM

2017-04-24 Thread Blanchette, J.C.
> On 24 Apr 2017, at 17:12, Andreas Lochbihler > 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

Re: [isabelle-dev] Uses of Jenkins at TUM

2017-04-24 Thread Makarius
On 24/04/17 17:12, Andreas Lochbihler 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.

Re: [isabelle-dev] Uses of Jenkins at TUM

2017-04-24 Thread Andreas Lochbihler
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. Andreas On 24/04/17 14:46, Makarius wrote: This is

[isabelle-dev] Uses of Jenkins at TUM

2017-04-24 Thread Makarius
This is another attempt to open a discussion about Jenkins at TUM. Are there users of it outside the TUM group? What is good about it? What is bad about it? Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de