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

[Lars Hupel]

> 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 workflow to
allow large-scale refactorings without perma-red builds.

Cheers
Lars
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Florian Haftmann]

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 in proximity have been considered as
>> one build job.  So maybe this is not important.
> 
> Sorry, I don't understand. You push some changeset and Jenkins will tell
> you exactly which Mercurial id is the current tip. What else do you need?

You may ignore my confusion safely.

> Right. That would be easier under the presence of a good
> "testboard_submit" command.
> 
> As I alluded to in my earlier email this is all well within the realm of
> possibility (even platform-independent desktop notifications upon
> completion), but it requires some dedicated implementation effort.

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.

Cheers,
Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Gerwin Klein]

> 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 you would get a predictable combination as well.
>
> Right, that's one option. I still consider that to need glue code,
> because you really don't want users to have to perform three pushes and
> an additional commit. Knowing myself I would only use that sort of
> workflow if it were automated.

True. That glue code could be local in that repo, though.

Cheers,
Gerwin



The information in this e-mail may be confidential and subject to legal 
professional privilege and/or copyright. National ICT Australia Limited accepts 
no liability for any damage caused by this email or its attachments.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Lars Hupel]

> 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 option. I still consider that to need glue code,
because you really don't want users to have to perform three pushes and
an additional commit. Knowing myself I would only use that sort of
workflow if it were automated.

Cheers
Lars
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Gerwin Klein]

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, at 07:40, Lars Hupel  wrote:
>
>>> 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 them simultaneously.
>
> It is – I'm not denying that. However, it is difficult to implement.
>
> I had a stab at it a while back and realised that I don't have time for
> a proper solution. In essence, you have to completely decouple the
> events "push to testboard" and "build change" and implement some glue
> logic both on the server and on the client side.
>
> If anyone wants to attempt it, I'm happy to explain how it should be
> implemented.
>
> Cheers
> Lars
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev




The information in this e-mail may be confidential and subject to legal 
professional privilege and/or copyright. National ICT Australia Limited accepts 
no liability for any damage caused by this email or its attachments.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[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 in proximity have been considered as
> one build job.  So maybe this is not important.

Sorry, I don't understand. You push some changeset and Jenkins will tell
you exactly which Mercurial id is the current tip. What else do you need?

> A notification to the committer(s) of the respective changesets.  Maybe
> Jenkins has already support for that?

It does, but currently neither of the following conditions apply:

1) both repositories observe the DVCS standard of including a valid
email address in the commit author string; or
2) we have a "testboard_submit" command which asks for an email address
or reads it from a configuration or uses desktop notifications; or
3) we can figure out which user pushed a change

> The workflow I am alluding to is as follows:
> a) You make a change to the distro.
> b) You have a rough idea what the consequences are and check the
> involved sessions after an analysis.
> c) You do some kind of plausibility checking (e.g. building HOL-Library)-
> d) You push optimistically to the testboard.
> e) Hence you get a rough idea what has still to be done in certain sessions.
> f) You check the corresponding sessions.
> g) Now you are ready for the next iteration.

Right. That would be easier under the presence of a good
"testboard_submit" command.

As I alluded to in my earlier email this is all well within the realm of
possibility (even platform-independent desktop notifications upon
completion), but it requires some dedicated implementation effort.

Cheers
Lars
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Lars Hupel]

>> 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 them simultaneously.

It is – I'm not denying that. However, it is difficult to implement.

I had a stab at it a while back and realised that I don't have time for
a proper solution. In essence, you have to completely decouple the
events "push to testboard" and "build change" and implement some glue
logic both on the server and on the client side.

If anyone wants to attempt it, I'm happy to explain how it should be
implemented.

Cheers
Lars
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Florian Haftmann]

>> 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. It is fixable, but not very high
> priority right now.

Well, it just means that there are no queued builds.  I agree that we
can easily live with that.

>> A disadvantage is that you have to click a lot to find out the hash id
>> in the distribution view. I guess that could be easily resolved by a
>> suitable configuration, or hosting the distribution testboard repository
>> in the same hosting environment as the AFP testboard repository.
> 
> An easier way is this: Go to  and
> on the bottom of the page, click on the appropriate testboard button. It
> will take you to an overview page of Jenkins where you can see the
> changes which triggered the build (including links to hgweb) and also
> links to the console outputs of the subjobs.

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 build job.  So maybe this is not important.

>> 5. Then repeatedly check the URI of the build until results are available.
> 
> What kind of notification would you envision here?

A notification to the committer(s) of the respective changesets.  Maybe
Jenkins has already support for that?

>> An inherent weakness of the testboard approach is that whenever you
>> gradually improve your changesets you to rebuild ab initio. But the
>> building times are compact enough that this shouldn't be too big a problem.
> 
> The new hardware brought the raw build time down to about an hour. An
> obvious optimisation would be to not clean before building. But then
> again, most often, changes being tested out affect Pure or HOL which
> means everything needs to be rebuilt anyway.

The workflow I am alluding to is as follows:
a) You make a change to the distro.
b) You have a rough idea what the consequences are and check the
involved sessions after an analysis.
c) You do some kind of plausibility checking (e.g. building HOL-Library)-
d) You push optimistically to the testboard.
e) Hence you get a rough idea what has still to be done in certain sessions.
f) You check the corresponding sessions.
g) Now you are ready for the next iteration.

As I said, I think we can live without any optimisation here at the moment.

Cheers,
Florian

> 
> Cheers
> Lars
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Florian Haftmann]

>> 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 distro
demands changes in the AFP, you want to test them simultaneously.

Cheers,
Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Lars Hupel]

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 is not ideal. It is fixable, but not very high
priority right now.

> A disadvantage is that you have to click a lot to find out the hash id
> in the distribution view. I guess that could be easily resolved by a
> suitable configuration, or hosting the distribution testboard repository
> in the same hosting environment as the AFP testboard repository.

An easier way is this: Go to  and
on the bottom of the page, click on the appropriate testboard button. It
will take you to an overview page of Jenkins where you can see the
changes which triggered the build (including links to hgweb) and also
links to the console outputs of the subjobs.

> 5. Then repeatedly check the URI of the build until results are available.

What kind of notification would you envision here?

> An inherent weakness of the testboard approach is that whenever you
> gradually improve your changesets you to rebuild ab initio. But the
> building times are compact enough that this shouldn't be too big a problem.

The new hardware brought the raw build time down to about an hour. An
obvious optimisation would be to not clean before building. But then
again, most often, changes being tested out affect Pure or HOL which
means everything needs to be rebuilt anyway.

Cheers
Lars
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Lars Hupel]

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 testboard
and AFP testboard together.

Cheers
Lars
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] An experience report on the testboard

[Florian Haftmann]

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« according to .hgrc is defined as
alias for
»!{ "${HG}" push -f testboard && "${HG}" phase --force --draft; }«

3. Go to https://ci.isabelle.systems/jenkins/job/testboard-afp/ and
await new build run to be scheduled.

4. Check that newly emerging build and compare the hash ids according to
http://isabelle.in.tum.de/repos/testboard/summary and
https://bitbucket.org/isa-afp/afp-testboard/commits/all

Here I encountered two problems:
* Even if pushes occur in close proximity, there is a chance that they
are not matched in that particular build.
* To resolve the situation, I did qpop and qpush, this creating patches
with different hash ids. But pushing that did not trigger a new run.
Don't know what's exactly going on here…
A disadvantage is that you have to click a lot to find out the hash id
in the distribution view. I guess that could be easily resolved by a
suitable configuration, or hosting the distribution testboard repository
in the same hosting environment as the AFP testboard repository.

5. Then repeatedly check the URI of the build until results are available.

An inherent weakness of the testboard approach is that whenever you
gradually improve your changesets you to rebuild ab initio. But the
building times are compact enough that this shouldn't be too big a problem.

Cheers,
Florian


-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev