On 06/10/2016 17:11, Makarius wrote:
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?
I can only guess what "nightly build" is: probably without the AFP. In which case I can only repeat what was said more than once: we want to test as much as possible in reasonable time, rather than with a delay of a day.
Add-on question: * Why is there a testboard at all, instead of plain ssh access?
For one thing it makes sure that enough is tested (eg incl AFP and latex). We find it very convenient.
A final point before I bow out. I am very grateful to Lars for setting up the test infrastructure. This does not contribute but distracts from his PhD work and his teaching duties. For that very reason he will tune Jenkins further as required but he will not spend much time on it.
TobiasPS I have recently talked to a number of mathematicians who had taken a serious look at Isabelle. Their main complaint was uniformly that the theories were unreadable because there was not enough plain latex text in them.
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
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
