[isabelle-dev] HOL-Analysis instability

[Manuel Eberl]

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
lxcisaX?

Manuel


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