[isabelle-dev] [Afp-submit] AFP build times out in file/theory presentation

[Fabian Huch]

There seems to be a performance degradation in the presentation 
somewhere between Isabelle/adb10e840b71 and Isabelle/2b212c8138a. I 
notified Makarius about that but didn't spot the error yet (there were 
lots of changes in the signature).

I think the jenkins build should be configured to send out notification 
emails in situations like that. Either by marking builds that time out 
as "failed" rather than "aborted" (which I'm in favour of) or by 
explicitly sending out emails on aborted builds (though it seems like it 
would send an email at every aborted built, not just the first one).

Fabian

On 11/16/21 09:16, Tobias Nipkow wrote:
> We are both right: in the log I looked at, the proofs only left 90 
> minutes for the presentation until timeout (hence no upper bound), but 
> as you point out, if the proofs are shorter, the presentation part 
> will happily use the rest of the 4 hours.
>
> Tobias
>
> On 16/11/2021 09:06, Gerwin Klein wrote:
>> I'm not sure it's that, although it might be related. The log looks 
>> like the presentation part went on for almost the full 4h, which sure 
>> isn't how long it is supposed to take.
>>
>> Cheers,
>> Gerwin
>>
>>> On 16 Nov 2021, at 19:02, Tobias Nipkow <nipkow at in.tum.de> wrote:
>>>
>>> Oops, hadn't noticed that. The hard timing facts: The presentation 
>>> part, which used to take 35-40 mins is now taking 90 minutes at 
>>> least, and we don't have an upper bound (because of the timeout). Of 
>>> course we could try to increase the timeout and see what happens. 
>>> The problem is largely due to the fact that theory presentation used 
>>> to be incremental (quite some time ago) but these days, even if only 
>>> 1 AFP entry has changed, the presentation for the entire AFP is built.
>>>
>>> Tobias
>>>
>>> On 16/11/2021 06:42, Gerwin Klein wrote:
>>>> It looks like since 12 Nov at isabelle at 2b212c8138a5 the AFP build 
>>>> has been timing out towards the end of theory/file presentation 
>>>> despite everything else being successful (logs at 
>>>> https://ci.isabelle.systems/jenkins/job/isabelle-all/3298/ for the 
>>>> morbidly curious). For some reason Jenkins decided that no emails 
>>>> needed to be sent for that.
>>>> I haven't been able to reproduce the problem locally, but this is 
>>>> happening even for small AFP changes where the proofs are finished 
>>>> after a few minutes, e.g. in 
>>>> https://ci.isabelle.systems/jenkins/job/isabelle-all/3301/consoleText 
>>>> (for afp-devel at 7c831b848ada135a and isabelle at 4f1c1c7eb95f4) so it's 
>>>> not the global timeout that is the issue. It does really seem to 
>>>> either hang or take very long for the presentation part.
>>>> To make testing worse, the entry Complex_Bounded_Operators is 
>>>> currently broken since (I think) Manuel's recent afp-devel commit 
>>>> 7aec7688b019. Manuel, could you please have a look at that?
>>>> In any case, I can't do the AFP release fork in this state, and 
>>>> will have to postpone until we've figured out what is going on with 
>>>> the presentation part.
>>>> Cheers,
>>>> Gerwin
>>>> _______________________________________________
>>>> Afp-submit mailing list
>>>> Afp-submit at mailman46.in.tum.de
>>>> https://mailman46.in.tum.de/mailman/listinfo/afp-submit
>>> _______________________________________________
>>> isabelle-dev mailing list
>>> isabelle-dev at in.tum.de
>>> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
>>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20211116/d2dc78c9/attachment-0001.htm>