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

[Gerwin Klein]

You were too fast :-), afp-devel is is for isabelle-devel, it shouldn't have isabelle-release changes in it.

It's unfortunate that isabelle-release has already diverged in content. Not a real problem, just a bit more overhead.

Ok, so I'll make an afp-2021-1 fork now, and it would be good if somebody could set up Jenkins to test this branch against isabelle-release. Lars used to do that -- I'm not sure who has taken over Jenkins.

After the fork we should temporarily revert that commit for Complex_Bounded_Operators in afp-devel (but keep it on afp-2021-1) until the release has happened. We should try to fix the timeout problem on the afp-2021-1/isabelle-release combination. After the release those changes will then be merged into both devel versions.

Cheers,
Gerwin


> On 16 Nov 2021, at 18:53, Manuel Eberl <manuel at pruvisto.org> wrote:
> 
> Have you tested Complex_Bounded_Operators with the latest isabelle-release? https://isabelle.sketis.net/repos/isabelle-release
> 
> That afp-devel push of mine was to adapt Complex_Bounded_Operators to the changes I had Makarius add to isabelle-release. At least on my machine it built fine.
> 
> Manuel
> 
> 
> 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
>> 
>> _______________________________________________
>> 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