On 10/13/2011 01:24 PM, Thomas Sewell wrote:
Good day all. Just wanted to let the Isabelle developers know about the latest
feature David Matthews has added to PolyML, and to let you all know how useful
it is.
The feature allows profiling of objects after garbage collection. When code is
On 10/13/2011 01:24 PM, Thomas Sewell wrote:
There are surprisingly many dummy tasks.
[...]
918632 Task_Queue.dummy_task(1)
val dummy_task = Task(NONE, ~1)
Values are not shared?! What the hell?
___
isabelle-dev mailing list
On Fri, 14 Oct 2011, Andreas Schropp wrote:
On 10/13/2011 01:24 PM, Thomas Sewell wrote:
There are surprisingly many dummy tasks.
[...]
918632 Task_Queue.dummy_task(1)
Such numbers always need to be put in relation. The original list was
like that:
918632
On 14/10/2011 09:13, Andreas Schropp wrote:
On 10/13/2011 01:24 PM, Thomas Sewell wrote:
Good day all. Just wanted to let the Isabelle developers know about
the latest feature David Matthews has added to PolyML, and to let you
all know how useful it is.
The feature allows profiling of objects
On 14/10/2011 10:56, Makarius wrote:
On Fri, 14 Oct 2011, Andreas Schropp wrote:
val dummy_task = Task(NONE, ~1)
Values are not shared?! What the hell?
Datatypes and tuples that contain only constant data are created once
during compilation.
This looks like an older version. Thomas was
On Fri, 14 Oct 2011, David Matthews wrote:
I can only guess that allocation of mutable stuff costs extra.
Allocation of a mutable, at least a fixed-size mutable such as ref,
doesn't cost any more than allocating an immutable. However, if a
mutable survives a GC it has an impact on
Good day all. Just wanted to let the Isabelle developers know about the latest
feature David Matthews has added to PolyML, and to let you all know how useful
it is.
The feature allows profiling of objects after garbage collection. When code is
compiled with PolyML.compiler.allocationProfiling
