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

[Tobias Nipkow]

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
> 
-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5579 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20211116/f1411934/attachment.bin>