<div dir="ltr"><div>A while ago this happened to me building CakeML. This thread might help you:</div><div><br></div><div><a href="https://www.mail-archive.com/polyml@inf.ed.ac.uk/msg01744.html">https://www.mail-archive.com/polyml@inf.ed.ac.uk/msg01744.html</a></div><div><br></div><div>- Gergely<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, 3 Dec 2019 at 17:35, Manuel Eberl <<a href="mailto:eberlm@in.tum.de">eberlm@in.tum.de</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">There have been a lot of spurious build failures of HOL-Analysis in our<br>
Jenkins CI [1,2] lately (cf. e.g. 6c208c2dca53). A quick glance at [3]<br>
seems to paint a similar picture. Linear_Programming int he AFP also<br>
fails spuriously. The error messages typically say<br>
<br>
  Run out of store - interrupting threads<br>
  *** Interrupt<br>
<br>
When it does go through, it seems to go through with a reasonable amount<br>
of time and memory. Also, this still seems to be happening after I split<br>
off HOL-Complex_Analysis from HOL-Analysis, which amounts to a 10%<br>
reduction in lines and elapsed time and 25% of GC time, so I would<br>
assume that it lowers the memory requirements quite a bit.<br>
<br>
But if anything, it seems to have made it worse: It seems that<br>
HOL-Analysis now fails almost every time. On my personal machine,<br>
HOL-Analysis never fails to build.<br>
<br>
I have no idea how to track down a problem like this.<br>
<br>
Cheers,<br>
<br>
Manuel<br>
<br>
[1]: <a href="https://ci.isabelle.systems/jenkins/job/isabelle-all/1553/consoleFull" rel="noreferrer" target="_blank">https://ci.isabelle.systems/jenkins/job/isabelle-all/1553/consoleFull</a><br>
[2]: <a href="https://ci.isabelle.systems/jenkins/job/isabelle-all/1571/consoleFull" rel="noreferrer" target="_blank">https://ci.isabelle.systems/jenkins/job/isabelle-all/1571/consoleFull</a><br>
[3]: <a href="https://isabelle.sketis.net/devel/build_status/" rel="noreferrer" target="_blank">https://isabelle.sketis.net/devel/build_status/</a><br>
_______________________________________________<br>
isabelle-dev mailing list<br>
<a href="mailto:isabelle-dev@in.tum.de" target="_blank">isabelle-dev@in.tum.de</a><br>
<a href="https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev" rel="noreferrer" target="_blank">https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev</a><br>
</blockquote></div>