On 06/10/16 17:03, Tobias Nipkow wrote: > Sorry, I don't consider them useless. > > Tobias > > On 06/10/2016 17:00, Makarius wrote: >> 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.
I need to be more specific: * Why is a plain "nightly build" done many times per day? (As immediate reaction on repository pushes.) * Why are testboard policies intermixed with "nightly build" policies? Add-on question: * Why is there a testboard at all, instead of plain ssh access? None of this has been seriously discussed so far. As far as I remember, the original Mira testboard was introduced in a situation, where builds became so slow and unwieldy that the mental model was changed to "batch-queue management" on a hypothetical computing cluster. Luckily, David Matthews saved us from that, and made everything small and fast again. Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev