[isabelle-dev] HOL-Analysis instability
eberlm at in.tum.de
Sun Dec 8 17:03:03 CET 2019
Were there any changes to the system or to HOL-Analysis since I asked?
HOL-Analysis seems to run much more reliably now. The last failure was 3
days and 8 builds ago. Back then it seemed to fail almost every time.
Or is it perhaps related to how much contention there is on the rest of
On 03/12/2019 21:15, Makarius wrote:
> On 03/12/2019 17:34, Manuel Eberl wrote:
>> Run out of store - interrupting threads
>> *** Interrupt
>> 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.
> It is also fine on my usual test machines, using --minheap 1500 and unbounded
> maxheap (thus 16G).
>> : https://ci.isabelle.systems/jenkins/job/isabelle-all/1553/consoleFull
>> : https://ci.isabelle.systems/jenkins/job/isabelle-all/1571/consoleFull
> Here I see --minheap 4G (a bit too much), --maxheap 8G (a bit too little),
> threads=4 (rather low) and -j10 (rather high). The many parallel processes can
> easily have a bad influence the special ones with singular resource requirements.
> I often use a machine for testing elsewhere that is a slightly faster than
> lxcisa at TUM, and both hardware nodes are available. On this machine the
> standard quasi-interactive build is rather fast and stable:
> ML_OPTIONS="--minheap 1500"
> isabelle build -N -j8 -o threads=8 -a
> Selective timings:
> Finished HOL (0:03:05 elapsed time, 0:10:04 cpu time, factor 3.27)
> Finished HOL-Analysis (0:05:57 elapsed time, 0:31:01 cpu time, factor 5.20)
> Finished HOL-Complex_Analysis (0:00:30 elapsed time, 0:02:56 cpu time, factor
> Total timing:
> 0:13:03 elapsed time, 5:14:57 cpu time, factor 24.13
More information about the isabelle-dev