[isabelle-dev] HOL-Analysis instability
immler at in.tum.de
Tue Dec 3 19:11:29 CET 2019
I also saw this failure while building 3548d54ce3ee on lxcisa0 with the
following command and ML_OPTIONS:
isabelle build -v -a -X slow -j8 -othreads=8
ML_OPTIONS="--minheap 1000 --maxheap 4000"
After the failure, another invocation of the same command built
everything without problems.
A wild guess: could be related to the fact that on the second attempt,
HOL-Analysis was the only session being built, whereas on the first
attempt there were lots of sessions (based on HOL) running in parallel.
On 12/3/2019 11:34 AM, Manuel Eberl 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 
> 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.
> : https://ci.isabelle.systems/jenkins/job/isabelle-all/1553/consoleFull
> : https://ci.isabelle.systems/jenkins/job/isabelle-all/1571/consoleFull
> : https://isabelle.sketis.net/devel/build_status/
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev