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

Makarius makarius at sketis.net
Fri Mar 29 11:15:23 CET 2019

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:


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


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


More information about the isabelle-dev mailing list