[isabelle-dev] NEWS: Update to Poly/ML 5.8 -- and towards Isabelle2019

[Makarius]

*** System ***

* Update to Poly/ML 5.8 allows to use the native x86_64 platform without
the full overhead of 64-bit values everywhere. This special x86_64_32
mode provides up to 16GB ML heap, while program code and stacks are
allocated elsewhere. Thus approx. 5 times more memory is available for
applications compared to old x86 mode (which is no longer used by
Isabelle). The switch to the x86_64 CPU architecture also avoids
compatibility problems with Linux and macOS, where 32-bit applications
are gradually phased out.


This refers to Isabelle/63721ee8c86c, it is now the official release of
Poly/ML 5.8 by David Matthews.

It all looks great so far, and there is still plenty of time for further
testing until the official release of Isabelle2019.

The present plan is to publish an unofficial Isabelle2019-RC0 snapshot
in early April, and start officially with Isabelle2019-RC1 at the
beginning of May. It all should be finalized an published until
15-Jun-2019, when I will go on travel (not vacation, but a visit to
colleagues in Paris).


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)

[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