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 _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
