[isabelle-dev] HOL-Analysis instability

[Gergely Buday]

A while ago this happened to me building CakeML. This thread might help you:

https://www.mail-archive.com/polyml@inf.ed.ac.uk/msg01744.html

- Gergely

On Tue, 3 Dec 2019 at 17:35, Manuel Eberl <eberlm at in.tum.de> wrote:

> There have been a lot of spurious build failures of HOL-Analysis in our
> Jenkins CI [1,2] lately (cf. e.g. 6c208c2dca53). A quick glance at [3]
> seems to paint a similar picture. Linear_Programming int he AFP also
> fails spuriously. The error messages typically say
>
>   Run out of store - interrupting threads
>   *** Interrupt
>
> When it does go through, it seems to go through with a reasonable amount
> of time and memory. Also, this still seems to be happening after I split
> off HOL-Complex_Analysis from HOL-Analysis, which amounts to a 10%
> reduction in lines and elapsed time and 25% of GC time, so I would
> assume that it lowers the memory requirements quite a bit.
>
> But if anything, it seems to have made it worse: It seems that
> HOL-Analysis now fails almost every time. On my personal machine,
> HOL-Analysis never fails to build.
>
> I have no idea how to track down a problem like this.
>
> Cheers,
>
> Manuel
>
> [1]: https://ci.isabelle.systems/jenkins/job/isabelle-all/1553/consoleFull
> [2]: https://ci.isabelle.systems/jenkins/job/isabelle-all/1571/consoleFull
> [3]: https://isabelle.sketis.net/devel/build_status/
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20191203/f2dc6861/attachment-0001.html>