[isabelle-dev] Fwd: [Isabelle-ci] Build failure in Isabelle (benchmark)

[Makarius]

On 28/03/2019 22:28, Lars Hupel wrote:
>>> "Unable to increase stack" is one of the various messages that tells
>>> you that PolyML has run out of resources. It doesn't really tell you
>>> what the problem is though. It might be an actual problem or a
>>> temporary problem caused by a machine being overloaded.
>>
>> This is likely connected to the recent change of platform. I will
>> investigate this; maybe bumping the memory limit will resolve it.
> 
> Even after the switch to x86_64_32, this session keeps failing.

There is indeed a remaining problem with polyml-5.8 here. See the
following measurements of non-failing test runs:

https://isabelle.sketis.net/devel/build_status/Linux_Benchmarks/index.html#session_HOL-Quickcheck_Benchmark
https://isabelle.sketis.net/devel/build_status/Linux_Benchmarks_2_threads/index.html#session_HOL-Quickcheck_Benchmark


I have made some quick tests. The problem appears to occur with
'find_unused_assms' here:

https://isabelle.sketis.net/repos/isabelle/file/tip/src/Benchmarks/Quickcheck_Benchmark/Find_Unused_Assms_Examples.thy#l22

This requires some precise profiling in sequential and parallel mode, to
pin it down to the real problem. (I will be still busy elsewhere in the
next few days).


	Makarius