[isabelle-dev] An experience report on the testboard

Gerwin Klein Gerwin.Klein at nicta.com.au
Tue Jul 5 01:45:54 CEST 2016


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 <hupel at in.tum.de> 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-dev at 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.



More information about the isabelle-dev mailing list