[isabelle-dev] Fwd: [Isabelle-ci] Build failure in AFP

[Manuel Eberl]

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 <ci at isabelle.systems>
> To: isabelle-ci at 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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20180831/f73f3d48/attachment-0002.html>