On 06/10/16 16:44, Tobias Nipkow wrote:
>
>> I also prefer to have AFP working all the time, but that would require
>> much more resources, both hardware and humans.
>
> For a growing number of Isabelle users, the AFP is just as important as
> the Isabelle repository. Hence the AFP needs to be tested and maintained
> just as much, which requires (at least) the hardware resources that we
> provide; we cannot dedicate half of it to manual testing.
This is actually my main point of criticism for the present situation:
the Jenkins setup uses a lot of hardware resources, by doing too many
useless tests. These resources are then missing for important tests, as
well as interactive sessions.
This can be easily changed by giving up these design decisions:
* quasi real-time reactivity (of what is actually a 1.5h batch build)
* exclusive "provisioning" of machines for Jenkins
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
