Re: [isabelle-dev] An experience report on the testboard

> What I see from this thread is that at some time we really have to talk > about official build orders with respective hg ids, either using > subrepos or whatever. That is accurate. So far we have largely avoided the need to do that, but with an ever growing AFP we need to figure out some

Re: [isabelle-dev] An experience report on the testboard

Am 04.07.2016 um 23:49 schrieb Lars Hupel: >> The problem I was referring to is that in order to get a deeper idea >> what's going on you want to have a look at the topology of the history. >> However I guess this is closely related to my surprise that not both >> patches to distro and AFP pushed

Re: [isabelle-dev] An experience report on the testboard

> On 5 Jul 2016, at 16:15, Lars Hupel wrote: > >> Another way of getting simultaneous tests would be to use subrepos. I.e. >> >> test-repo/ >> isabelle/ (subrepo) >> afp/ (subrepo) >> >> The trigger would then be the push to test-repo, not to any of the subrepos, >> and

Re: [isabelle-dev] An experience report on the testboard

> Another way of getting simultaneous tests would be to use subrepos. I.e. > > test-repo/ >isabelle/ (subrepo) >afp/ (subrepo) > > The trigger would then be the push to test-repo, not to any of the subrepos, > and you would get a predictable combination as well. Right, that's one

Re: [isabelle-dev] An experience report on the testboard

Another way of getting simultaneous tests would be to use subrepos. I.e. test-repo/ isabelle/ (subrepo) afp/ (subrepo) The trigger would then be the push to test-repo, not to any of the subrepos, and you would get a predictable combination as well. Cheers, Gerwin > On 5 Jul 2016,

Re: [isabelle-dev] An experience report on the testboard

> The problem I was referring to is that in order to get a deeper idea > what's going on you want to have a look at the topology of the history. > However I guess this is closely related to my surprise that not both > patches to distro and AFP pushed in proximity have been considered as > one

Re: [isabelle-dev] An experience report on the testboard

>> This is currently not implemented. Isabelle testboard will always use >> AFP devel and vice versa. It is not possible to test Isabelle testboard >> and AFP testboard together. > > But I regard this as a central use case: if a change to the distro > demands changes in the AFP, you want to test

Re: [isabelle-dev] An experience report on the testboard

>> 3. Go to https://ci.isabelle.systems/jenkins/job/testboard-afp/ and >> await new build run to be scheduled. > > There can currently only be one testboard build running at a time. That > means you should wait to push until the previous run is finished. > > I understand that this is not ideal.

Re: [isabelle-dev] An experience report on the testboard

>> 1. Changesets to dist and AFP exist as hg patches. > > This is currently not implemented. Isabelle testboard will always use > AFP devel and vice versa. It is not possible to test Isabelle testboard > and AFP testboard together. But I regard this as a central use case: if a change to the

Re: [isabelle-dev] An experience report on the testboard

To add to my last mail: > 3. Go to https://ci.isabelle.systems/jenkins/job/testboard-afp/ and > await new build run to be scheduled. There can currently only be one testboard build running at a time. That means you should wait to push until the previous run is finished. I understand that this

Re: [isabelle-dev] An experience report on the testboard

Hi Florian, thanks for your feedback! Commenting in some more detail will take me some time, but for now a quick reply: > 1. Changesets to dist and AFP exist as hg patches. This is currently not implemented. Isabelle testboard will always use AFP devel and vice versa. It is not possible to test