Update: I pushed another changeset and now everything is green again (if you excuse the pun).
I tracked the problem to a diverging invocation of "blast": https://bitbucket.org/isa-afp/afp-devel/src/e15414dceb2836d07d50546ee94ff8083fbcc80d/thys/Green/Derivs.thy?at=default&fileviewer=file-view-default#Derivs.thy-165 However, this "blast" does not diverge on any of my machines, no matter if single-threaded or multi-threaded, no matter if "isabelle build" or Isabelle/jEdit. It actually terminates almost instantaneously. It does, however, seem to diverge reliably on the Testboard, on the workermtahpc, and on isabelle-server. I found this "blast" invocation by running "isabelle jedit" on isabelle-server via XForwarding, and there it was continuously purple and remained purple forever. I have no idea why it does that; the proof in question is actually very simple. It does use "continuous_intros" and my changeset does introduce a few new "continuous_intros" rules and also some "intro" rules, but none of them match the goal here at all, so I cannot see how that would influence anything. And I am certainly stumped as to how this kind of non-deterministic behaviour could come about. Manuel On 8/31/18 1:34 AM, Manuel Eberl wrote: > It seems that my latest commit f443ec10447d causes nontermination of the > AFP entry "Green". > > I saw this timeout on the testboard, but everything worked fine locally > despite trying several times, so I thought it was perhaps some spurious > issue and pushed the commit anyway. > > Unfortunately, "Green" seems to time out on Jenkins every time now. > Seeing as a while ago, we had spurious timeout issues that went away > when we increased the timeout, I tried doubling the timeout on the > Testboard (to 20 minutes!) and that did not help either. > > For comparison, on my modest machine, the entry needs a very reasonable > 2 minutes (both CPU and wall clock) when run with 1 thread, so >20 > minutes seems quite absurd. > > I looked at the entry in Isabelle/jEdit and found some invocations of > blast/force that took up to 8 seconds, but that should not be a problem. > > Does anyone have any idea what is going on here or how I could track > down this issue? > > Manuel > > > -------- Forwarded Message -------- > Subject: [Isabelle-ci] Build failure in AFP > Date: Thu, 30 Aug 2018 22:53:44 +0200 (CEST) > From: Isabelle/Jenkins <firstname.lastname@example.org> > To: isabelle...@mail46.informatik.tu-muenchen.de > > The AFP build failed. See the log at: > https://ci.isabelle.systems/jenkins/job/isabelle-all/288/ > > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev