[isabelle-dev] Nonterminating AFP build

[Tobias Nipkow]

This requires Johannes' expertise, but he is away for a few days.

Tobias

On 12/05/2016 12:58, Lawrence Paulson wrote:
> There are multiple failures in PMF_OF_List. It looks like the behaviour of simplification has changed concerning the functions ennreal and ereal.
> Larry
>
>> On 12 May 2016, at 11:39, Lawrence Paulson <lp15 at cam.ac.uk> wrote:
>>
>> It has no timeout, sorry, that was my fault. Now set to 300 seconds.
>>
>> We don’t need a global timeout, but why not a default timeout? We could set up to the median runtime. Actually I think our typical value of 600 seconds is much too high, considering that a loop in a common library could make dozens of entries run forever.
>> Larry
>>
>>> On 11 May 2016, at 23:58, Gerwin Klein <Gerwin.Klein at nicta.com.au> wrote:
>>>
>>> If it doesn’t have a timeout set, then that’s a mistake and should be fixed. It’d be good to have protection for all builds, not only through Jenkins.
>>>
>>> We’ve avoided a global timeout so far, because it’d have to be fairly long, i.e. if you have a few entries that don’t terminate because of a change in Isabelle for instance, you might very quickly be looking at multiple days.
>>>
>>> Might still be a good idea to add one anyway as an additional safety net.
>>>
>>> Cheers,
>>> Gerwin
>>>
>>>
>>>
>>>> On 12.05.2016, at 06:58, Lars Hupel <hupel at in.tum.de> wrote:
>>>>
>>>> Isabelle/8326aa594273
>>>> AFP/ffea2c11f257
>>>>
>>>> We appear to have an issue with nonterminating builds. See here:
>>>> <https://ci.isabelle.systems/jenkins/job/afp-repo-afp/189/consoleFull>.
>>>> I had to manually kill the running poly process. I'm not quite sure
>>>> which session causes it, but it's possibly Randomised_Social_Choice. I
>>>> was under the assumption that all AFP sessions had timeouts set –
>>>> apparently this is not the case.
>>>>
>>>> In order to avoid these problems in the future, I'll implement job
>>>> timeouts in Jenkins.
>>>>
>>>> Cheers
>>>> Lars
>>>> _______________________________________________
>>>> isabelle-dev mailing list
>>>> isabelle-dev at in.tum.de
>>>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>>>
>>>
>>> ________________________________
>>>
>>> The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
>>> _______________________________________________
>>> isabelle-dev mailing list
>>> isabelle-dev at in.tum.de
>>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>>
>
> _______________________________________________
> 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/20160512/e489b66a/attachment.bin>