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
