[isabelle-dev] Jenkins maintenance

[Tobias Nipkow]

On 06/10/2016 14:34, Makarius wrote:
> On 03/10/16 17:12, Manuel Eberl wrote:
>> It would also be an effective safeguard against breaking the repository (and possibly even the AFP),
>> which /does/ happen quite frequently. (cf. the current situation where
>> things have been broken for days)
>
> 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.

Leaving the AFP entries broken actually increases the human resources required 
to fix them later.

> A broken Isabelle repository is different: it means all wheels stand
> still.

Both for the repository and the AFP, everything is selective. Most people do not 
suffer if HOL-Proofs does not build, for example. Just as many AFP entries are 
irrelevant to most of us. But in the end we want all of it to work.

Tobias

> That can be easily avoided by spending about 20min with manual
> tests before pushing -- on decent hardware.
>
> When the Isabelle repository is broken, which happens about 2 times per
> year, there are friendly mails on isabelle-dev about it, mostly
> reminders of README_REPOSITORY. Can you point out a mail thread, where
> anybody was seriously blamed for it?
>
>
>> Another improvement I can think of is
>> that it would be good to have a little more control over testing:
>> aborting tests when they are not necessary anymore, testing only the
>> repository (and not the AFP) etc. All of this we can talk about and find
>> a solution in time.
>
> Yes. I read it as: ssh access to a proper test machine. That is the
> traditional Isabelle development model.
>
> When the Prover IDE learns to use remote machines eventually, that will
> also use ssh for direct interaction with jobs.
>
>
>> The reality of it all is that our testing infrastructure was in shambles for
>> quite some time. Then Lars came along and put in a lot of effort to get
>> things up and running again. The main response on this mailing list were
>> vague insinuations that he does not understand how to do tests, or does
>> not care about doing it properly, which could hardly be farther removed
>> from the truth.
>
> I had many private discussions with Lars in the past few months. I even
> pointed out important requirements before the start of the Jenkins project.
>
> The present situation is that we have no proper test environment after
> isatest was shutdown prematurely. This is what I have called "flying
> blind", because vital performance measurements are missing.
>
> I need to improvise something for the coming release -- which is the
> reason why I have been off-line for some days, and also postponed the
> start of the hot phase for Isabelle2016-1.
>
>
> 	Makarius
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>

-------------- 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/20161006/bdfd548a/attachment.bin>