<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body text="#000000" bgcolor="#FFFFFF">
<p><font size="+1">Update: I pushed another changeset and now
everything is green again (if you excuse the pun).</font></p>
<p><font size="+1">I tracked the problem to a diverging invocation
of "blast":
<a class="moz-txt-link-freetext" href="https://bitbucket.org/isa-afp/afp-devel/src/e15414dceb2836d07d50546ee94ff8083fbcc80d/thys/Green/Derivs.thy?at=default&fileviewer=file-view-default#Derivs.thy-165">https://bitbucket.org/isa-afp/afp-devel/src/e15414dceb2836d07d50546ee94ff8083fbcc80d/thys/Green/Derivs.thy?at=default&fileviewer=file-view-default#Derivs.thy-165</a></font></p>
<p><font size="+1">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.<br>
</font></p>
<p><font size="+1">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.</font></p>
<p><font size="+1">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.</font></p>
<p><font size="+1">Manuel</font></p>
<p><font size="+1"><br>
</font></p>
<div class="moz-cite-prefix">On 8/31/18 1:34 AM, Manuel Eberl wrote:<br>
</div>
<blockquote type="cite"
cite="mid:0ce1c78b-09af-1b21-9676-0cf38392923c@in.tum.de">
<pre class="moz-quote-pre" wrap="">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 <a class="moz-txt-link-rfc2396E" href="mailto:ci@isabelle.systems"><ci@isabelle.systems></a>
To: <a class="moz-txt-link-abbreviated" href="mailto:isabelle-ci@mail46.informatik.tu-muenchen.de">isabelle-ci@mail46.informatik.tu-muenchen.de</a>
The AFP build failed. See the log at:
<a class="moz-txt-link-freetext" href="https://ci.isabelle.systems/jenkins/job/isabelle-all/288/">https://ci.isabelle.systems/jenkins/job/isabelle-all/288/</a>
</pre>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<pre class="moz-quote-pre" wrap="">_______________________________________________
isabelle-dev mailing list
<a class="moz-txt-link-abbreviated" href="mailto:isabelle-dev@in.tum.de">isabelle-dev@in.tum.de</a>
<a class="moz-txt-link-freetext" href="https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev</a>
</pre>
</blockquote>
</body>
</html>