[isabelle-dev] HOL-Analysis instability
eberlm at in.tum.de
Tue Dec 3 17:34:44 CET 2019
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 
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
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.
More information about the isabelle-dev