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