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 <[email protected]> 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@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@7c831b848ada135a and isabelle@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 >> [email protected] >> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev > _______________________________________________ > isabelle-dev mailing list > [email protected] > https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
