[isabelle-dev] Jenkins maintenance

[Tobias Nipkow]

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.

Tobias

PS 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
>

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5135 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20161007/bf0d4a0d/attachment.bin>