Email Gateway (Nov 16 2021 at 05:42): Email Gateway (Nov 16 2021 at 05:42):From: Gerwin Klein <kleing@unsw.edu.au>
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
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Nov 16 2021 at 07:53):From: Manuel Eberl <manuel@pruvisto.org>
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
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Nov 16 2021 at 08:16):From: Gerwin Klein <kleing@unsw.edu.au>
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
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Nov 16 2021 at 08:37):From: Fabian Huch <huch@in.tum.de>
On 11/16/21 09:16, Gerwin Klein wrote:
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.
I'm responsible for that now and will set that up.
Fabian
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,
GerwinOn 16 Nov 2021, at 18:53, Manuel Eberl <manuel@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@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
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Nov 16 2021 at 08:42):From: Gerwin Klein <kleing@unsw.edu.au>
Perfect, thanks. The push is still running, turns out the afp has grown quite
a bit. Will let you know when it's there.
Cheers,
Gerwin
Email Gateway (Nov 16 2021 at 09:08):From: Gerwin Klein <kleing@unsw.edu.au>
<ssh://hg@foss.heptapod.net/isa-afp/afp-2021-1> is now available.
Cheers,
Gerwin
Email Gateway (Nov 16 2021 at 09:31):From: Fabian Huch <huch@in.tum.de>
Appropriate build job is also online:
https://ci.isabelle.systems/jenkins/job/isabelle-2021-1/
Fabian
Email Gateway (Nov 16 2021 at 11:24):From: Makarius <makarius@sketis.net>
On 16/11/2021 09:16, Gerwin Klein wrote:
You were too fast :-), afp-devel is is for isabelle-devel, it shouldn't have isabelle-release changes in it.
We have had this time of uncertainty of the pair isabelle-dev vs. afp-devel
after the fork of isabelle-dev to isabelle-release routinely in the past few
years.
From the Isabelle side, the "window of uncertainty" is only 30min .. 2h. For
AFP we often had many days, sometimes 1-2 weeks (IIRC).
So can this be organized in a better way?
E.g. have the "call to finalize AFP" earlier in the process and maybe have a
separate "afp-release" fork for it.
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.
Note that I will occasionally merge isabelle-release back to isabelle-dev
before final lift-off. It will happen within 2-3 days, for example.
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Nov 16 2021 at 23:14):From: Gerwin Klein <kleing@unsw.edu.au>
On 16 Nov 2021, at 22:24, Makarius <makarius@sketis.net> wrote:
On 16/11/2021 09:16, Gerwin Klein wrote:
You were too fast :-), afp-devel is is for isabelle-devel, it shouldn't have isabelle-release changes in it.
We have had this time of uncertainty of the pair isabelle-dev vs. afp-devel
after the fork of isabelle-dev to isabelle-release routinely in the past few
years.From the Isabelle side, the "window of uncertainty" is only 30min .. 2h. For
AFP we often had many days, sometimes 1-2 weeks (IIRC).So can this be organized in a better way?
E.g. have the "call to finalize AFP" earlier in the process and maybe have a
separate "afp-release" fork for it.
You're right that the uncertainty period is not really ideal. It relies on there not being any major content changes in isabelle-release. Often that works fine, but occasionally content drift does happen as it did this cycle.
What I've usually done in the past (and now) when content drift occurs, is what you suggest, i.e. an afp-release fork, which here is directly getting the name afp-2021-1. It can get that name, because the model for the AFP is that the release remains a separate fork, so what now operates as the pre-release fork will become the official release fork when everything is done.
We could remove the uncertainty period by always doing that and coordinating on the fork time. I'd be happy to try that out for the next release.
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.
Note that I will occasionally merge isabelle-release back to isabelle-dev
before final lift-off. It will happen within 2-3 days, for example.
That is nice, and makes the situation with afp-devel a bit easier to manage (the smaller the merge in the end, the less work there is at the actual release point).
Cheers,
Gerwin
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Last updated: Apr 25 2024 at 08:20 UTC