<html>
  <head>
    <meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
  </head>
  <body>
    <p>There seems to be a performance degradation in the presentation
      somewhere between Isabelle/adb10e840b71 and Isabelle/2b212c8138a.
      I notified Makarius about that but didn't spot the error yet
      (there were lots of changes in the signature).<br>
    </p>
    <p>I think the jenkins build should be configured to send out
      notification emails in situations like that. Either by marking
      builds that time out as "failed" rather than "aborted" (which I'm
      in favour of) or by explicitly sending out emails on aborted
      builds (though it seems like it would send an email at every
      aborted built, not just the first one).<br>
    </p>
    <p>Fabian<br>
    </p>
    <div class="moz-cite-prefix">On 11/16/21 09:16, Tobias Nipkow wrote:<br>
    </div>
    <blockquote type="cite"
      cite="mid:bb8cff23-bf3f-1ef5-b796-52ed3833295f@in.tum.de">We are
      both right: in the log I looked at, the proofs only left 90
      minutes for the presentation until timeout (hence no upper bound),
      but as you point out, if the proofs are shorter, the presentation
      part will happily use the rest of the 4 hours.
      <br>
      <br>
      Tobias
      <br>
      <br>
      On 16/11/2021 09:06, Gerwin Klein wrote:
      <br>
      <blockquote type="cite">I'm not sure it's that, although it might
        be related. The log looks like the presentation part went on for
        almost the full 4h, which sure isn't how long it is supposed to
        take.
        <br>
        <br>
        Cheers,
        <br>
        Gerwin
        <br>
        <br>
        <blockquote type="cite">On 16 Nov 2021, at 19:02, Tobias Nipkow
          <a class="moz-txt-link-rfc2396E" href="mailto:nipkow@in.tum.de"><nipkow@in.tum.de></a> wrote:
          <br>
          <br>
          Oops, hadn't noticed that. The hard timing facts: The
          presentation part, which used to take 35-40 mins is now taking
          90 minutes at least, and we don't have an upper bound (because
          of the timeout). Of course we could try to increase the
          timeout and see what happens. The problem is largely due to
          the fact that theory presentation used to be incremental
          (quite some time ago) but these days, even if only 1 AFP entry
          has changed, the presentation for the entire AFP is built.
          <br>
          <br>
          Tobias
          <br>
          <br>
          On 16/11/2021 06:42, Gerwin Klein wrote:
          <br>
          <blockquote type="cite">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
            <a class="moz-txt-link-freetext" href="https://ci.isabelle.systems/jenkins/job/isabelle-all/3298/">https://ci.isabelle.systems/jenkins/job/isabelle-all/3298/</a>
            for the morbidly curious). For some reason Jenkins decided
            that no emails needed to be sent for that.
            <br>
            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
            <a class="moz-txt-link-freetext" href="https://ci.isabelle.systems/jenkins/job/isabelle-all/3301/consoleText">https://ci.isabelle.systems/jenkins/job/isabelle-all/3301/consoleText</a>
            (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.
            <br>
            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?
            <br>
            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.
            <br>
            Cheers,
            <br>
            Gerwin
            <br>
            _______________________________________________
            <br>
            Afp-submit mailing list
            <br>
            <a class="moz-txt-link-abbreviated" href="mailto:Afp-submit@mailman46.in.tum.de">Afp-submit@mailman46.in.tum.de</a>
            <br>
            <a class="moz-txt-link-freetext" href="https://mailman46.in.tum.de/mailman/listinfo/afp-submit">https://mailman46.in.tum.de/mailman/listinfo/afp-submit</a>
            <br>
          </blockquote>
          _______________________________________________
          <br>
          isabelle-dev mailing list
          <br>
          <a class="moz-txt-link-abbreviated" href="mailto:isabelle-dev@in.tum.de">isabelle-dev@in.tum.de</a>
          <br>
          <a class="moz-txt-link-freetext" href="https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev">https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev</a>
          <br>
        </blockquote>
        <br>
      </blockquote>
      <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://mailman46.in.tum.de/mailman/listinfo/isabelle-dev">https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev</a>
</pre>
    </blockquote>
  </body>
</html>