On Tue, 18 Oct 2011, Thomas Sewell wrote:
My email about PolyML and memory usage has generated some discussion,
perhaps I should give some more context.
The continuing improvements of Poly/ML statistics add important new
aspects to the overall performance monitoring of Isabelle performance,
On Tue, 18 Oct 2011, Thomas Sewell wrote:
We've been running PolyML in 32 bit mode on most of our machines. As
images grow beyond 4GB, we must switch to 64 bit mode, which roughly
doubles memory use to 8GB, which means replacing most of our laptops.
The jump from 32bit to 64bit has to be
Hi all,
Many of us have already seen isatest and other failures with of the
following form:
/tmp/mira/workbench/26748-140130062513920/Isabelle/lib/scripts/run-polyml:
line 77: 13588 Killed $POLY -q $ML_OPTIONS
...
make: ***
Am 19.10.2011 um 22:34 schrieb Alexander Krauss:
Does anybody know if there is a straightforward translation of the error
codes 134/137 into English?
Just Google Unix exit codes.
E.g. 134 = The job is killed with an abort signal, and you probably got core
dumped, 137 = The job was killed