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

[isabelle-dev] An experience report on the testboard

Hi all, I have started to use the testboard and want to excite feedback on my workflow, as well as hint to certain inconveniences in the current setup. 1. Changesets to dist and AFP exist as hg patches. 2. In both repositories: hg push_to_testboard where »push_to_testboard«