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

[Makarius]

On 13/03/2019 21:06, 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.

BTW, with Poly/ML 5.8 being official, you can avoid full x86_64 for most
applications and always use the default x86_64_32.

This saves a lot of resources: I usually have ML_OPTIONS="--minheap
1500" with an open upper end -- the implicit limit is approx. 16G.

Even some entries of the slow/large groups of AFP work well with
x86_64_32, but I usually throw them into on big x86_64 pot as a special
case.

Another remaining application of full x86_64 is the huge PIDE session
forked by "isabelle dump" and related tools: it can require 64GB
(excluding slow), and I have not explored the upper end yet.


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Lars Hupel]

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


Cheers
Lars
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Thomas Sewell]

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

Cheers,
Thomas.

On 2019-03-12 12:14, Lawrence Paulson wrote:
Does anybody know what this is?

01:58:19 Running HOL-Quickcheck_Benchmark ...01:58:20 HOL-Quickcheck_Benchmark: 
theory HOL-Quickcheck_Benchmark.Needham_Schroeder_Base01:58:20 
HOL-Quickcheck_Benchmark: theory 
HOL-Quickcheck_Benchmark.Find_Unused_Assms_Examples01:58:23 
HOL-Quickcheck_Benchmark: theory 
HOL-Quickcheck_Benchmark.Needham_Schroeder_Guided_Attacker_Example01:58:24 
HOL-Quickcheck_Benchmark: theory 
HOL-Quickcheck_Benchmark.Needham_Schroeder_No_Attacker_Example01:58:24 
HOL-Quickcheck_Benchmark: theory 
HOL-Quickcheck_Benchmark.Needham_Schroeder_Unguided_Attacker_Example02:12:01 
Warning - Unable to increase stack - interrupting thread02:12:01 *** 
Interrupt02:12:01 HOL-Quickcheck_Benchmark FAILED

Larry

> Begin forwarded message:
>
> From: Isabelle/Jenkins 
> Subject: [Isabelle-ci] Build failure in Isabelle (benchmark)
> Date: 12 March 2019 at 01:22:32 GMT
> To: 
> isabelle...@mail46.informatik.tu-muenchen.de
>
> The Isabelle build failed. See the log at: 
> https://ci.isabelle.systems/jenkins/job/isabelle-nightly-benchmark/887/
> ___
> Isabelle-ci mailing list
> isabelle...@mail46.informatik.tu-muenchen.de
> https://mailman46.informatik.tu-muenchen.de/mailman/listinfo/isabelle-ci

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Lawrence Paulson]

Does anybody know what this is?

01:58:19 Running HOL-Quickcheck_Benchmark ...01:58:20 HOL-Quickcheck_Benchmark: 
theory HOL-Quickcheck_Benchmark.Needham_Schroeder_Base01:58:20 
HOL-Quickcheck_Benchmark: theory 
HOL-Quickcheck_Benchmark.Find_Unused_Assms_Examples01:58:23 
HOL-Quickcheck_Benchmark: theory 
HOL-Quickcheck_Benchmark.Needham_Schroeder_Guided_Attacker_Example01:58:24 
HOL-Quickcheck_Benchmark: theory 
HOL-Quickcheck_Benchmark.Needham_Schroeder_No_Attacker_Example01:58:24 
HOL-Quickcheck_Benchmark: theory 
HOL-Quickcheck_Benchmark.Needham_Schroeder_Unguided_Attacker_Example02:12:01 
Warning - Unable to increase stack - interrupting thread02:12:01 *** 
Interrupt02:12:01 HOL-Quickcheck_Benchmark FAILED

Larry

> Begin forwarded message:
> 
> From: Isabelle/Jenkins 
> Subject: [Isabelle-ci] Build failure in Isabelle (benchmark)
> Date: 12 March 2019 at 01:22:32 GMT
> To: isabelle...@mail46.informatik.tu-muenchen.de
> 
> The Isabelle build failed. See the log at: 
> https://ci.isabelle.systems/jenkins/job/isabelle-nightly-benchmark/887/

build.log
Description: Binary data
> ___
> Isabelle-ci mailing list
> isabelle...@mail46.informatik.tu-muenchen.de
> https://mailman46.informatik.tu-muenchen.de/mailman/listinfo/isabelle-ci

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev