[isabelle-dev] HOL-Analysis instability

[Makarius]

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:

  Isabelle/d411d5c84a4b

  ML_PLATFORM="x86_64_32-linux"
  ML_HOME="/home/makarius/.isabelle/contrib/polyml-5.8.1-20191124/x86_64_32-linux"
  ML_SYSTEM="polyml-5.8.1"
  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
5.86)

Total timing:
0:13:03 elapsed time, 5:14:57 cpu time, factor 24.13


	Makarius