[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 <https://ci.isabelle.systems/status/> 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-dev at 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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20160704/27191d9f/attachment.sig>