<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>