[isabelle-dev] HOL-Analysis instability

Makarius makarius at sketis.net
Tue Dec 3 21:15:02 CET 2019

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).

> [1]: https://ci.isabelle.systems/jenkins/job/isabelle-all/1553/consoleFull
> [2]: 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 mailing list